<div dir="ltr"><div dir="ltr"><br></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Sun, 18 Aug 2019 at 20:32, Alexey Sidorin <<a href="mailto:alexey.v.sidorin@ya.ru">alexey.v.sidorin@ya.ru</a>> wrote:</div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
Just some field notes. This design has a very important feature - <br>
reproducible analysis. If we had this split, the warnings were always <br>
the same independently on the checkers enabled or disabled. <br>
Unfortunately, without this feature, the analysis depends on what <br>
checkers can terminate the analysis path or add additional transitions <br>
making warnings of the same checker different if different checkers are <br>
enabled within it.<br></blockquote><div><br></div><div>I very much agree with you, though this issue is a tough nut to crack. Say that my esoteric codebase manages to fool a checker that emits fatal error nodes, I may want to disable that checker altogether, diagnostics and modeling included, as it screws with the rest of the analysis as well. I lean on the side of not directly exposing modeling checkers to the users to tinker with, but unfortunately we're far off from being so precise that we could confidently make this a developer only feature.</div><div><br></div><div>On the other hand, I only heard of such an issue with one of our internal checkers, that introduced practically infinite state splits, so I can't confidently say that this is a common problem either. Do you guys have any experience with this?</div></div></div>