unsoundness due to packed structs

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

---

Id	Project	Category	View	Due Date	Updated
ID0000719	Frama-C	Kernel	public	2011-02-13	2014-02-12

Reporter	regehr	Assigned To	monate	Resolution	fixed
Priority	normal	Severity	minor	Reproducibility	always
Platform	-	OS	-	OS Version	-
Product Version	Frama-C Carbon-20110201	Target Version	-	Fixed in Version	Frama-C Nitrogen-20111001

Description :

Analyzing the attached program like this:

toplevel.opt -val -slevel 14 foo_pp.c

Gives output including this:

    g_113.f0 ? {2240865284; }
         .f1 ? {-540177875780372926; }
         .f2 ? {-1; }
         .f3 ? {0; }
         .f4 ? {-1; }
         .[bits 184 to 191] ? UNINITIALIZED
         .f5 ? {-1; }
         .f6 ? {-5796648127719171460; }

g_113 is of type S0 which is declared using the pack(1) pragma, which makes all fields 1-byte aligned, so there should be no padding.

Not packing the struct properly causes Frama-C to have an incorrect impression about its layout.

Perhaps a very strongly-worded warning should appear in the output if the pack pragma is encountered in a program, but not honored.

Attachments

• foo_pp.c