Frama-C Bug Tracking System - Frama-C
View Issue Details
0000832Frama-CKernelpublic2011-05-24 08:242014-02-12 16:59
pascal 
virgile 
normalminoralways
closedfixed 
Frama-C GIT, precise the release id 
Frama-C Nitrogen-20111001 
0000832: r13586 Spurious "assert \separated(...)" (csmith)
file 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.
No tags attached.
related to 0000771closed virgile r12436, unnecessary warning for side-effects (csmith) 
Issue History
2011-05-24 08:24pascalNew Issue
2011-05-24 08:24pascalStatusnew => assigned
2011-05-24 08:24pascalAssigned To => virgile
2011-05-24 08:25pascalSummarySpurious "assert \separated(...)" => r13586 Spurious "assert \separated(...)" (csmith)
2011-05-24 08:27pascalRelationship addedrelated to 0000771
2011-05-24 08:53virgileStatusassigned => acknowledged
2011-05-24 18:25svnCheckin
2011-05-24 18:25svnStatusacknowledged => resolved
2011-05-24 18:25svnResolutionopen => fixed
2011-10-10 14:13signolesFixed in Version => Frama-C Nitrogen-20111001
2011-10-10 14:14signolesStatusresolved => closed
2011-10-21 14:47pascalStatusclosed => feedback
2011-10-21 14:47pascalResolutionfixed => reopened
2011-10-21 14:47pascalCategoryPlug-in > value analysis => Kernel
2011-10-21 14:48pascalStatusfeedback => closed
2011-10-21 14:48pascalResolutionreopened => fixed
2014-02-12 16:59Note Added: 0004783
2014-02-12 16:59Statusclosed => resolved

Notes
(0004783)
   
2014-02-12 16:59   
Fix committed to stable/neon branch.