Frama-C Bug Tracking System - Frama-C
View Issue Details
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.
Relationships
related to 0000771closed virgile r12436, unnecessary warning for side-effects (csmith) 
Attached Files

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

Issue History
Date ModifiedUsernameFieldChange
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:25svn
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
2013-12-19 01:12Source_changeset_attached => framac master 54758d8a
2014-02-12 16:54Source_changeset_attached => framac stable/neon 54758d8a
2014-02-12 16:59Note Added: 0004783
2014-02-12 16:59Statusclosed => resolved