<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
</head>
<body bgcolor="#FFFFFF" text="#000000">
<div class="moz-cite-prefix">23.08.2019 15:50, Kristóf Umann пишет:<br>
</div>
<blockquote type="cite"
cite="mid:CAGcXOD7STn4JDteDcg2CZCBBRp_mxtUw9uKtUq-r+93j_hxLfQ@mail.gmail.com">
<meta http-equiv="content-type" content="text/html; charset=UTF-8">
<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"
moz-do-not-send="true">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>
</blockquote>
<p><br>
</p>
<p>Yes, we often seen this problem when introducing a new
path-sensitive checker or disabling some. This usually lead to
some warnings of other checkers appear or disappear. The only
solution we had is to fix the checker set we run analyzer with but
it didn't work if a new checker is added.<br>
</p>
</body>
</html>