2020-12-05 00:26 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0001448Frama-CPlug-in > Evapublic2014-03-13 15:57
ReporterAnne 
Assigned Toyakobowski 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
Product VersionFrama-C Fluorine-20130501 
Target VersionFixed in VersionFrama-C Neon-20140301 
Summary0001448: Interpretation of @ assigns \result;
DescriptionSorry 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.
TagsNo tags attached.
Attached Files

-Relationships
+Relationships

-Notes

~0003977

Anne (reporter)

Last edited: 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 (manager)

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 (reporter)

Yes : that would be a good idea since otherwise, results can seem strange...

~0004062

yakobowski (manager)

Value will now warn for all missing '\from' part, and each time no 'assigns \result' is specified and this result is used.
+Notes

-Issue History
Date Modified Username Field Change
2013-06-20 17:51 Anne New Issue
2013-06-20 17:51 Anne Status new => assigned
2013-06-20 17:51 Anne Assigned To => yakobowski
2013-06-20 17:54 Anne Note Added: 0003977
2013-06-20 17:54 Anne Note Edited: 0003977
2013-06-20 18:07 yakobowski Note Added: 0003978
2013-06-21 10:50 Anne Note Added: 0003979
2013-09-06 20:55 yakobowski Note Added: 0004062
2013-09-06 21:57 svn
2013-09-06 21:57 svn Status assigned => resolved
2013-09-06 21:57 svn Resolution open => fixed
2014-03-13 15:56 signoles Fixed in Version => Frama-C Neon-20140301
2014-03-13 15:57 signoles Status resolved => closed
2018-01-12 14:26 signoles Category Plug-in > value analysis => Plug-in > Eva
+Issue History