GitLab

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.