<div dir="ltr">Has anybody considered somehow configuring the analyzer to treat asserts like calls to clang_analyzer_eval? If I understand correctly, that would enable it to report when assertions were obviously false? (of course, then it'd produce a ton of TRUEs and UNKNOWNs too...)<br></div><div class="gmail_extra"><br clear="all"><div><div class="gmail_signature"><div dir="ltr"><div><div dir="ltr"><span style="font-size:12.8000001907349px">Sincerely,</span><br style="font-size:12.8000001907349px"><span style="font-size:12.8000001907349px">Alexander Riccio</span><br style="font-size:12.8000001907349px"><span style="font-size:12.8000001907349px">--</span><br style="font-size:12.8000001907349px"><span style="font-size:12.8000001907349px">"Change the world or go home."</span><div style="font-size:12.8000001907349px"><a href="http://about.me/ariccio" target="_blank">about.me/ariccio</a></div><div style="font-size:12.8000001907349px"><a href="http://about.me/ariccio" target="_blank"><br></a></div><div style="font-size:12.8000001907349px">If left to my own devices, I will build more.</div><div style="font-size:12.8000001907349px">⁂</div></div></div></div></div></div>
<br><div class="gmail_quote">On Fri, Apr 8, 2016 at 2:08 PM, Devin Coughlin <span dir="ltr"><<a href="mailto:dcoughlin@apple.com" target="_blank">dcoughlin@apple.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div style="word-wrap:break-word"><br><div><span class=""><blockquote type="cite"><div>On Apr 7, 2016, at 6:47 PM, Alexander Riccio <<a href="mailto:test35965@gmail.com" target="_blank">test35965@gmail.com</a>> wrote:</div><br><div><div><div><div style="font-family:Calibri,sans-serif;font-size:11pt">I remember seeing something about the static analyzer checking asserts in the docs, how well does that actually work?<br></div></div></div></div></blockquote><div><br></div></span><div>Just to be clear, unlike many verification tools, the analyzer doesn’t “check” asserts. In verification-speak, it treats an assert like an assume. That is, if you have:</div><div><br></div><div>1: int *x = NULL;</div><div>2: assert(x != NULL);</div><div>3: *x = 7;</div><div><br></div><div>The analyzer will *not* warn that the assertion will definitely fail at line 2.</div><div><br></div><div>Instead, because assert(condition) is typically defined as a macro to expand to something like:</div><div><br></div><div>if (!condition) {</div><div>  ...</div><div>  exit(-1);</div><div>}</div><div><br></div><div>The assert will cause the analyzer to explore two paths: one where the condition doesn’t hold and exit() is called and one where the condition is assumed to hold and execution continues.</div><div><br></div><div>As Artem described, the analyzer will stop exploring the exit() path because exit() is noreturn.  But in this case, the analyzer will also stop exploring the path where the condition holds (i.e., x != NULL). This is because along that path the analyzer also knows x == NULL (from line 1).  This is a contradiction, which the analyzer interprets to mean the path is infeasible and so it will stop exploring this path as well. Ultimately this means the analyzer will not warn about the null pointer dereference at line 3.</div><div><br></div><div>By the way, there is a webpage describing how the analyzer deals with custom assertions at <<a href="http://clang-analyzer.llvm.org/annotations.html#custom_assertions" target="_blank">http://clang-analyzer.llvm.org/annotations.html#custom_assertions</a>>.</div><span class="HOEnZb"><font color="#888888"><div><br></div><div>Devin</div></font></span></div></div></blockquote></div><br></div>