Interpretation of @ assigns \result;
ID0001448: This issue was created automatically from Mantis Issue 1448. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0001448 | Frama-C | Plug-in > Eva | public | 2013-06-20 | 2014-03-13 |
| Reporter | Anne | Assigned To | yakobowski | Resolution | fixed |
| Priority | normal | Severity | minor | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Fluorine-20130501 | Target Version | - | Fixed in Version | Frama-C Neon-20140301 |
Description :
Sorry for the title which is not very informative, but here is the problem : in this example :
//@ assigns \result; extern char * get_ptr (void); int main (void) { char * p = get_ptr (); int x = p ? 0 : 1; return x; }
The value analysis tells me that the else branch is dead, so x is always 0. If I change the assigns property into : //@ assigns \result \from \nothing; The problem disappears.