Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001114Frama-CKernelpublic2012-03-10 16:512014-02-12 16:59
Reporterpascal 
Assigned Tovirgile 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C GIT, precise the release id 
Target VersionFixed in VersionFrama-C Oxygen-20120901 
Summary0001114: 17514, -unspecified-access and if (*p = (*p < 3)) (csmith)
DescriptionIn the program below, line 6 is as innocuous as line 5, but:

$ bin/toplevel.opt -val -unspecified-access t.c
[kernel] preprocessing with "gcc -C -E -I. t.c"
t.c:6:[kernel] warning: Unspecified sequence with side effect:
                  /* <- *p p */
                  tmp = *p < 3;
                  /* *p <- tmp p */
                  *p = tmp;
...
t.c:6:[kernel] warning: undefined multiple accesses in expression. assert \separated(p, p);;


int x, *p;

main(){
  p = &x;
  *p = (*p < 3);
  if (*p = (*p < 3))
    x = 4;
}
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0004711)

2014-02-12 16:59

Fix committed to stable/neon branch.

- Issue History
Date Modified Username Field Change
2012-03-10 16:51 pascal New Issue
2012-03-10 16:52 pascal Status new => assigned
2012-03-10 16:52 pascal Assigned To => virgile
2012-03-10 16:53 pascal Description Updated
2012-03-27 18:17 svn Checkin
2012-03-27 18:17 svn Status assigned => resolved
2012-03-27 18:17 svn 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
2014-02-12 16:59 Note Added: 0004711
2014-02-12 16:59 Status closed => resolved


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker