Results differ between value analysis and GCC on bitfields
ID0000890: This issue was created automatically from Mantis Issue 890. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0000890 | Frama-C | Plug-in > Eva | public | 2011-07-25 | 2014-02-12 |
| Reporter | monate | Assigned To | pascal | Resolution | fixed |
| Priority | normal | Severity | major | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C GIT, precise the release id | Target Version | - | Fixed in Version | Frama-C Nitrogen-20111001 |
Description :
On 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.