<html><head><meta http-equiv="Content-Type" content="text/html charset=utf-8"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;" class=""><br class=""><div><blockquote type="cite" class=""><div class="">On Apr 7, 2016, at 6:47 PM, Alexander Riccio <<a href="mailto:test35965@gmail.com" class="">test35965@gmail.com</a>> wrote:</div><br class="Apple-interchange-newline"><div class=""><meta http-equiv="Content-Type" content="text/html; charset=utf-8" class=""><div class=""><div class=""><div style="font-family: Calibri,sans-serif; font-size: 11pt;" class="">I remember seeing something about the static analyzer checking asserts in the docs, how well does that actually work?<br class=""></div></div></div></div></blockquote><div><br class=""></div><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 class=""></div><div>1: int *x = NULL;</div><div>2: assert(x != NULL);</div><div>3: *x = 7;</div><div><br class=""></div><div>The analyzer will *not* warn that the assertion will definitely fail at line 2.</div><div><br class=""></div><div>Instead, because assert(condition) is typically defined as a macro to expand to something like:</div><div><br class=""></div><div>if (!condition) {</div><div> ...</div><div> exit(-1);</div><div>}</div><div><br class=""></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 class=""></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 class=""></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" class="">http://clang-analyzer.llvm.org/annotations.html#custom_assertions</a>>.</div><div><br class=""></div><div>Devin</div></div></body></html>