Hi,
Ok yeah, there are different ways to look at that.
(1) First things first, are you reading the actual analyzer output? It should explain to you step-by-step what the analyzer is thinking. Static analyzer warnings are absolutely meaningless without the full output. Eg. --analyzer-output text gives you:
test.cpp:14:13: note: Assuming 'a' is not equal to field 'num'
if (a == num)
^~~~~~~~
test.cpp:14:9: note: Taking false branch
if (a == num)
^
test.cpp:19:13: note: Assuming 'a' is equal to field 'num'
if (a != num)
^~~~~~~~
test.cpp:19:9: note: Taking false branch
if (a != num)
^
test.cpp:21:19: note: Division by zero
return 10 / (a - num);
~~~^~~~~~~~~~~
1 warning generated.
(2) The warning is indeed a false positive, because the last return-statement is provably dead code. Namely, because map.clear() does not change the value of field num, the false branch cannot be taken at if (a != num).
Note that even though map.clear() does not change that value, doesn’t mean it could not. Theoretically speaking, if it was any other method on any other class, it could have the capacity to mutate num through safe pointer arithmetic, something along the lines of
void MyClass::clear() {
int *num_addr = ((char *)this) + offsetof(DivZeroCheckerTestClass, num)
- offsetof(DivZeroCheckerTestClass, map);
*num_addr = 123;
}
So it’s part of the contract of std::map::clear() that it doesn’t do that. Unfortunately the static analyzer doesn’t hardcode the contract for all standard library methods, so it doesn’t know that this can’t happen.
(3) The static analyzer is correct to assert that “the code 10 / (a - num) always divides by zero when executed”. The code literally verifies that it’s dividing by zero before division. Even though it’s currently a vacuous truth (the code is never executed), the code clearly doesn’t make sense.
Note, however, that it’s not possible to statically prove that the code is not dead. It can sometimes notice that the code is dead (like it should have in this example) but if it doesn’t notice anything like that, there’s still an irrefutable suspicion that the code may be dead. No matter how hard you read the code, you may always run into a situation when “this entire app is never run” or “this library is never linked against” or something like that.
Any static analysis can only ever find code that doesn’t make sense. Any promise that bugs it finds can be hit at runtime, is a lie.
In this sense, this warning isn’t much worse than any other warning emitted by the static analyzer. It has successfully found code that doesn’t make sense. In the general case you can’t really ask for more.
In this case, of course, we could have done better.
(4) The best solution in this case could be to simply warn the user about dead code, instead of division by zero. That would avoid the confusion, provide helpful warning, and if users don’t care about dead code they could turn it off separately.
Unfortunately, our analysis technique (symbolic execution without merges) isn’t suitable for reliably detecting dead code, as detecting dead code requires reasoning about all possible execution paths in the program. Our analysis, on the contrary, tries to explore as many paths as possible but never promises to explore all of them (of which there may be infinite).
So, we could totally implement dead code warnings with a different technique, but they’ll never play together nicely and reliably. That dream of cross-checking one warning with the other isn’t likely to come true (though it can work pretty well in some cases, including this one).
(5) A more realistic solution would be to model standard library methods more precisely. In particular, we can make sure they don’t invalidate our knowledge of unrelated fields in the class. We already know how to do that in theory, eg. we know about const, as @jankorous pointed out. So this shouldn’t be too hard to implement.
(6) Another possible way to discard this warning comes from our plan to generally be more wary of execution paths that rely on taking opposite assumptions about important values after invalidation (like this, further discussion). Even though such warnings can be correct, they usually either aren’t, or can be found on other paths that don’t follow the offending pattern (in which case we’ll keep showing them).