Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001448Frama-CPlug-in > value analysispublic2013-06-20 17:512014-03-13 15:57
ReporterAnne 
Assigned Toyakobowski 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
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

-  Notes
(0003977)
Anne (reporter)
2013-06-20 17:54
edited on: 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)
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 (reporter)
2013-06-21 10:50

Yes : that would be a good idea since otherwise, results can seem strange...
(0004062)
yakobowski (manager)
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.

- 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 Checkin
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


Copyright © 2000 - 2017 MantisBT Team
Powered by Mantis Bugtracker