[cfe-dev] [analyzer] RFC, garbage value => out of bounds

[Artem Dergachev via cfe-dev]

The problem that nr has not been proven to be greater than 2 was already 
covered by Joerg; it's worth it to have a look at the html diagnostic 
for the original case to see if it was proven that such caller context 
exists, otherwise we shouldn't ideally be seeing this warning. In fact, 
probably a heuristic based on detecting 
SymbolRegionValue<VarRegoin{ParmVarDecl}>-like values and staying more 
conservative with them than with other values may work somehow, not sure.

 > the a[i] value is not undefined when i is out of bounds.

Out of bounds access causes undefined behavior. In practice, the program 
either crashes or produces an undefined value. I agree that the term 
"uninitialized" may not quite make sense here though.

The analyzer ideally should stop analysis of the branch (in this example 
there's only one branch, so the whole analysis interrupts) after 
undefined behavior occurs - which is what enabling array bounds checker 
should cause. Because array bounds checker is alpha (not sure why), the 
analysis continues, modeling the undefined value read by a pointer to 
perfectly defined array (which doesn't make the value, say, a[2] 
defined) with an undefined symbolic-value marker (UndefinedVal), and 
then another checker warns on usage of such undefined value.

So the problem we run into here is that the original message is much 
clearer in a simple case of:

   void foo() {
     int n;
     bar(n) // Function call argument is an uninitialized value
   }

In this example i'd certainly prefer "uninitialized" over "undefined". 
In your example, i'd probably prefer "undefined", and certainly prefer a 
significantly different warning, such as "Function call argument is a 
garbage value [obtained from an out-of-bound array access]". 
Unfortunately, discriminating between these two cases is right now 
technically difficult (the signleton UndefinedVal object does not 
provide any origin information). Then, again, we should not have seen 
this warning, because due to undefined behavior the execution shouldn't 
reach here anyway.

And i guess that there aren't many places when you can obtain undefined 
values without first causing undefined behavior. Uninitialized values 
are certainly one of such rare places. Though better warnings would be 
great anyway.

Maybe it's worth it to turn UndefinedVal into a true symbol in order to 
properly track its origin?