insufficient preconditions given to verify constructor call from global variable initialization
ID0002003: This issue was created automatically from Mantis Issue 2003. Further discussion may take place here.
|ID0002003||Frama-Clang||Plug-in > clang||public||2014-12-01||2015-05-04|
|Product Version||-||Target Version||-||Fixed in Version||-|
The predonditions of the cls() constructor aren't verified for the call originating from the declaration in line 9. The goal in the .mlw file is just "forall i : int. is_sint32(i) -> (0 <> i)", i.e. the fact that i (that is x in the C++ source) has the value 2 isn't given as precondition.
In contrast, when cls() is called explicitly in main(), the actual value of x is given - the .mlw file's goal for line 13 reads: "... -> (0 <> (safe_comp_div(1, 2)))". Note that here the effect of the line-9 cls()-call is ignored in x-value computation; in fact, already the cls()-call in line 12 will crash with zero-divide.
This issues is probably closely related to #2002.