Wrong AST (csmith)

ID0000933: This issue was created automatically from Mantis Issue 933. Further discussion may take place here.

---

Id	Project	Category	View	Due Date	Updated
ID0000933	Frama-C	Kernel	public	2011-08-23	2014-02-12

Reporter	pascal	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 :

Mini:~/d $ cat r.c int g_18;

typedef unsigned int uint32_t; typedef int int32_t; typedef short int16_t; typedef long long int64_t;

struct S0 { uint32_t f0; int16_t f1; signed f2 : 26; int64_t f3; };

union U3 { signed f0 : 7; int32_t f1; int32_t f2; struct S0 f3; };

static union U3 g_7[1] = {{0x00868BB4L}};

int g_5; int g_2;

void Frama_C_show_each(unsigned);

main(){ unsigned short l_8 = 1UL; unsigned int l_16 = 0xBD4AA41AL;

g_2 |= (g_7[g_5].f3.f2 = l_16); Frama_C_show_each(g_2); }

Mini:~/d $ ~/ppc/bin/toplevel.opt -val -slevel 99 r.c | grep each [value] Called Frama_C_show_each({3175785498})

Mini:~/d $ clang -m32 r.c show_each.c && ./a.out r.c:29:1: warning: type specifier missing, defaults to 'int' [-Wimplicit-int] main(){ ^ 1 warning generated. [value] Called Frama_C_show_each({21668890})

Mini:~/d $ ~/ppc/bin/toplevel.opt -print r.c [kernel] preprocessing with "gcc -C -E -I. r.c" r.c:34:[kernel] warning: Body of function main falls-through. Adding a return statement /* Generated by Frama-C */ typedef unsigned int uint32_t; typedef int int32_t; typedef short int16_t; typedef long long int64_t; struct S0 { uint32_t f0 ; int16_t f1 ; int f2 : 26 ; int64_t f3 ; }; union U3 { int f0 : 7 ; int32_t f1 ; int32_t f2 ; struct S0 f3 ; }; int g_18; static union U3 g_7[1] = {{(int)0x00868BB4L}}; int g_5; int g_2; extern void Frama_C_show_each(unsigned int); int main(void) { int __retres; unsigned short l_8; unsigned int l_16; int attribute((FRAMA_C_BITFIELD_SIZE(26))) tmp; l_8 = (unsigned short)1UL; l_16 = (unsigned int)0xBD4AA41AL; { /undefined sequence/ tmp = (int)l_16; g_7[g_5].f3.f2 = tmp; g_2 |= tmp; } Frama_C_show_each((unsigned int)g_2); __retres = 0; return (__retres); }

The program displayed with -print is not equivalent to the original because attribute((FRAMA_C_BITFIELD_SIZE(26))) in the declaration of tmp does not have any semantics.