2021-01-18 17:36 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0000888Frama-CKernelpublic2014-02-12 16:54
Reporterpascal 
Assigned Tovirgile 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
Product VersionFrama-C GIT, precise the release id 
Target VersionFixed in VersionFrama-C Oxygen-20120901 
Summary0000888: 14292: warn for unspecified side-effect that are separated by a function call (csmith)
Description~ $ 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);
}
TagsNo tags attached.
Attached Files

-Relationships
+Relationships

-Notes

~0002046

pascal (reporter)

To clarify, I think there is no need to warn here, but the analysis does (precision bug).
+Notes

-Issue History
Date Modified Username Field Change
2011-07-25 12:03 pascal New Issue
2011-07-25 12:03 pascal Status new => assigned
2011-07-25 12:03 pascal Assigned To => virgile
2011-07-25 12:42 pascal Note Added: 0002046
2012-03-28 15:24 svn
2012-06-10 00:24 yakobowski Status assigned => resolved
2012-06-10 00:24 yakobowski Resolution open => fixed
2012-09-19 17:15 signoles Fixed in Version => Frama-C Oxygen-20120901
2012-09-19 17:16 signoles Status resolved => closed
2013-12-19 01:12 Source_changeset_attached => framac master 31f08f7e
2014-02-12 16:54 Source_changeset_attached => framac stable/neon 31f08f7e
+Issue History