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.