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 - 2017 MantisBT Team
Powered by Mantis Bugtracker