Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000832Frama-CKernelpublic2011-05-24 08:242014-02-12 16:59
Reporterpascal 
Assigned Tovirgile 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C GIT, precise the release id 
Target VersionFixed in VersionFrama-C Nitrogen-20111001 
Summary0000832: r13586 Spurious "assert \separated(...)" (csmith)
Descriptionfile t.c: int a, *G; int g(int x, int y) { return x + y; } main(int c, char **v){ G = &a; *G = (a < (g((0U || (((a ^ a) <= a) < ((*G) || a))), 5))); return a; } $ ~/ppc/bin/toplevel.byte -val -unspecified-access t.c t.c:13:[kernel] warning: Unspecified sequence with side effect: /* <- a G *G */ if (*G) { tmp = 1; } else { if (a) { tmp = 1; } else { tmp = 0; } } /* <- a a a */ /* <- */ tmp_0 = g((((a ^ a) <= a) < tmp) != 0,5); /* *G <- G a */ *G = a < tmp_0; ... t.c:13:[kernel] warning: undefined multiple accesses in expression. assert \separated(G,& a); t.c:13:[kernel] warning: undefined multiple accesses in expression. assert \separated(G,G); ... The program is completely defined, g has no side-effects.
TagsNo tags attached.
Attached Files

- Relationships
related to 0000771closedvirgile r12436, unnecessary warning for side-effects (csmith) 

-  Notes
(0004783)

2014-02-12 16:59

Fix committed to stable/neon branch.

- Issue History
Date Modified Username Field Change
2011-05-24 08:24 pascal New Issue
2011-05-24 08:24 pascal Status new => assigned
2011-05-24 08:24 pascal Assigned To => virgile
2011-05-24 08:25 pascal Summary Spurious "assert \separated(...)" => r13586 Spurious "assert \separated(...)" (csmith)
2011-05-24 08:27 pascal Relationship added related to 0000771
2011-05-24 08:53 virgile Status assigned => acknowledged
2011-05-24 18:25 svn Checkin
2011-05-24 18:25 svn Status acknowledged => resolved
2011-05-24 18:25 svn Resolution open => fixed
2011-10-10 14:13 signoles Fixed in Version => Frama-C Nitrogen-20111001
2011-10-10 14:14 signoles Status resolved => closed
2011-10-21 14:47 pascal Status closed => feedback
2011-10-21 14:47 pascal Resolution fixed => reopened
2011-10-21 14:47 pascal Category Plug-in > value analysis => Kernel
2011-10-21 14:48 pascal Status feedback => closed
2011-10-21 14:48 pascal Resolution reopened => fixed
2014-02-12 16:59 Note Added: 0004783
2014-02-12 16:59 Status closed => resolved


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker