Clang SA false positive

Hi All,

I came across a curious pattern of FPs while evaluating Clang SA:

$ cat garbageread-fp.c
1. extern void printInt(int x); // prints int
3. static int zero = 0;
5. void f() {
6. int x;
7. if (zero != 0)
8. printInt(0); // dead code
9. else
10. x = 0;
11. if (zero == 0) {
12. if (!x)
13. printInt(x);
14. }
15. }

$ clang --analyze garbageread-fp.c
garbageread-fp.c:12:8: warning: Branch condition evaluates to a garbage
        if (!x)
1 warning generated.

I have uploaded an html report here: JS Bin - Collaborative JavaScript Debugging

Why does Clang SA forget the constraint down the execution path?

1. Replacing static with extern retains the FP.
2. The FP has something to do with function inlining. Replacing printInt
with standard library function makes the FP go away!



The static analyzer can only reason about one translation unit at once. With only local knowledge the static analyzer can not assume that zero is not modified by the time f is called. For this reason I think the analyzer evaluates both branches of your first if. On the branch, where zero is not 0 it calls into printInt. The definition of printInt is not available, so the analyzer have to assume that, the value of zero is changed. Why? Because even though it is static and printInt should not be able to modify it, printInt might be able to call into another function which can modify the value of zero. So by the time you reach the second if statment on this branch you do not have any reliable information about the value of zero. The reason why it work with standard functions is that, there are some heuristics which assumes that standard library functions are well behaved and do not modify global state. All in all it all boils down to that it is impossible to reason about global state rigorously with local knowledge. This problem could be mitigated using some annotations that some functions are not going to modify the global state.

I hope I could answer your question.