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.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0002003 | Frama-Clang | Plug-in > clang | public | 2014-12-01 | 2015-05-04 |
| Reporter | Jochen | Assigned To | virgile | Resolution | open |
| Priority | normal | Severity | minor | Reproducibility | always |
| Platform | frama-c-Neon-20140301+dev-stance | OS | - | OS Version | xubuntu-cfe13.10 |
| Product Version | - | Target Version | - | Fixed in Version | - |
Description :
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.