[cfe-dev] Reporting false positives detected by Clang staticanalyzer

[<Alexander G. Riccio> via cfe-dev]

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...)

Sincerely,
Alexander Riccio
--
"Change the world or go home."
about.me/ariccio

<http://about.me/ariccio>
If left to my own devices, I will build more.
⁂

On Fri, Apr 8, 2016 at 2:08 PM, Devin Coughlin <dcoughlin at apple.com> wrote:

>
> On Apr 7, 2016, at 6:47 PM, Alexander Riccio <test35965 at gmail.com> wrote:
>
> I remember seeing something about the static analyzer checking asserts in
> the docs, how well does that actually work?
>
>
> 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:
>
> 1: int *x = NULL;
> 2: assert(x != NULL);
> 3: *x = 7;
>
> The analyzer will *not* warn that the assertion will definitely fail at
> line 2.
>
> Instead, because assert(condition) is typically defined as a macro to
> expand to something like:
>
> if (!condition) {
>   ...
>   exit(-1);
> }
>
> 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.
>
> 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.
>
> By the way, there is a webpage describing how the analyzer deals with
> custom assertions at <
> http://clang-analyzer.llvm.org/annotations.html#custom_assertions>.
>
> Devin
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/cfe-dev/attachments/20160412/6a3b9a5e/attachment.html>