Frama-C Bug Tracking System - Frama-C
View Issue Details
0001448Frama-CPlug-in > Evapublic2013-06-20 17:512014-03-13 15:57
Anne 
yakobowski 
normalminoralways
closedfixed 
Frama-C Fluorine-20130501 
Frama-C Neon-20140301 
0001448: Interpretation of @ assigns \result;
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.
No tags attached.
Issue History
2013-06-20 17:51AnneNew Issue
2013-06-20 17:51AnneStatusnew => assigned
2013-06-20 17:51AnneAssigned To => yakobowski
2013-06-20 17:54AnneNote Added: 0003977
2013-06-20 17:54AnneNote Edited: 0003977
2013-06-20 18:07yakobowskiNote Added: 0003978
2013-06-21 10:50AnneNote Added: 0003979
2013-09-06 20:55yakobowskiNote Added: 0004062
2013-09-06 21:57svnCheckin
2013-09-06 21:57svnStatusassigned => resolved
2013-09-06 21:57svnResolutionopen => fixed
2014-03-13 15:56signolesFixed in Version => Frama-C Neon-20140301
2014-03-13 15:57signolesStatusresolved => closed
2018-01-12 14:26signolesCategoryPlug-in > value analysis => Plug-in > Eva

Notes
(0003977)
Anne   
2013-06-20 17:54   
I suddenly remember that you (Boris) told me to always put a \from property on pointers. That must be the problem : but maybe you should emit a big warning on that because it is confusing...
(0003978)
yakobowski   
2013-06-20 18:07   
In this case, Value cannot easily complain: your 'assigns \result' is transformed into 'assigns \nothing' by the kernel. But we should probably complain whenever the return type contains pointers and no from is used to specify it.
(0003979)
Anne   
2013-06-21 10:50   
Yes : that would be a good idea since otherwise, results can seem strange...
(0004062)
yakobowski   
2013-09-06 20:55   
Value will now warn for all missing '\from' part, and each time no 'assigns \result' is specified and this result is used.