Frama-C Bug Tracking System - Frama-C
View Issue Details
0000888Frama-CKernelpublic2011-07-25 12:032014-02-12 16:54
pascal 
virgile 
normalminoralways
closedfixed 
Frama-C GIT, precise the release id 
Frama-C Oxygen-20120901 
0000888: 14292: warn for unspecified side-effect that are separated by a function call (csmith)
~ $ ppc/bin/toplevel.opt -val u.c -unspecified-access ... u.c:5:[kernel] warning: undefined multiple accesses in expression. assert \separated(& x,& x); ... ~ $ cat u.c int f(int); main(){ int x; x = f(x=2); }
No tags attached.
Issue History
2011-07-25 12:03pascalNew Issue
2011-07-25 12:03pascalStatusnew => assigned
2011-07-25 12:03pascalAssigned To => virgile
2011-07-25 12:42pascalNote Added: 0002046
2012-03-28 15:24svnCheckin
2012-06-10 00:24yakobowskiStatusassigned => resolved
2012-06-10 00:24yakobowskiResolutionopen => fixed
2012-09-19 17:15signolesFixed in Version => Frama-C Oxygen-20120901
2012-09-19 17:16signolesStatusresolved => closed

Notes
(0002046)
pascal   
2011-07-25 12:42   
To clarify, I think there is no need to warn here, but the analysis does (precision bug).