Frama-C Bug Tracking System - Frama-C
View Issue Details
0000890Frama-CPlug-in > Evapublic2011-07-25 18:022014-02-12 16:59
Reportermonate 
Assigned Topascal 
PrioritynormalSeveritymajorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C GIT, precise the release id 
Target VersionFixed in VersionFrama-C Nitrogen-20111001 
Summary0000890: Results differ between value analysis and GCC on bitfields
DescriptionOn the program
==bug.i==============
union U0 {
   unsigned short f0 ;
   int f1 ;
   int f2 : 5 ;
   unsigned char const f3 ;
};

unsigned short G0 ;
int G1 ;
int G2;
unsigned char G3 ;
union U0 G={(unsigned short)65532U};
int main() {
  G0=G.f0;
  G1=G.f1;
  G2=G.f2;
  G3=G.f3;
  printf("%d %d %d %d : %d\n",G0,G1,G2,G3,G2==-4);
  return (G2==-4);
}
=========================

frama-c -val bug.i
returns:
===
[value] Values for function main:
          G0 ? {65532}
          G1[bits 0 to 15] ? {65532}
            [bits 16 to 31] ? {0}
          G2 ? {28}
          G3# ? {65532} misaligned 0%16
          __retres ? {0}
===

but gcc bug.i && ./a.out ; echo $?
displays :
===
65532 65532 -4 252 : 1
1
===
They do not agree on the result nor on the value of G2.
TagsNo tags attached.
parent of 0000871closed monate scfed program behaves differently from original 
Attached Files

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

Issue History
2011-07-25 18:02monateNew Issue
2011-07-25 18:02monateStatusnew => assigned
2011-07-25 18:02monateAssigned To => pascal
2011-07-25 18:03monateRelationship addedparent of 0000871
2011-07-25 23:40svn
2011-07-25 23:40svnStatusassigned => resolved
2011-07-25 23:40svnResolutionopen => fixed
2011-10-10 14:13signolesFixed in Version => Frama-C Nitrogen-20111001
2011-10-10 14:14signolesStatusresolved => closed
2013-12-19 01:12pascalSource_changeset_attached => framac master 8ead7999
2014-02-12 16:54pascalSource_changeset_attached => framac stable/neon 8ead7999
2014-02-12 16:59pascalNote Added: 0004761
2014-02-12 16:59pascalStatusclosed => resolved
2018-01-12 14:26signolesCategoryPlug-in > value analysis => Plug-in > Eva