Frama-C Bug Tracking System - Frama-C
View Issue Details
IDProjectCategoryView StatusDate SubmittedLast Update
0000719Frama-CKernelpublic2011-02-13 05:472014-02-12 16:59
Reporterregehr 
Assigned Tomonate 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Carbon-20110201 
Target VersionFixed in VersionFrama-C Nitrogen-20111001 
Summary0000719: unsoundness due to packed structs
DescriptionAnalyzing 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.
TagsNo tags attached.
Relationships
Attached Filesc foo_pp.c (54,091) 2011-02-13 05:47
https://bts.frama-c.com/file_download.php?file_id=172&type=bug

Notes
(0001488)
pascal   
2011-02-13 06:47   
I have re-categorized this as a kernel issue. In presence of the "offsetof" macro, if affects all plug-ins, even if they do not otherwise think about memory in such concrete terms.

If the pack pragma applies to the entire target code, then the solution is simply a matter of defining a new target platform with different alignment parameters. There is a C program that you can compile with the pragma to get a new platform description automatically.

If the pack pragma applies only to some structs inside the target program, then the front-end would have to be deeply modified to accommodate support for the pragma. Considering the workaround above, we will wait until the need is expressed before undertaking these changes.

But yes, a warning would be nice.
(0004799)
monate   
2014-02-12 16:59   
Fix committed to stable/neon branch.

Issue History
Date ModifiedUsernameFieldChange
2011-02-13 05:47regehrNew Issue
2011-02-13 05:47regehrStatusnew => assigned
2011-02-13 05:47regehrAssigned To => pascal
2011-02-13 05:47regehrFile Added: foo_pp.c
2011-02-13 06:39pascalCategoryPlug-in > value analysis => Kernel
2011-02-13 06:39pascalProduct VersionFrama-C GIT, precise the release id => Frama-C Carbon-20110201
2011-02-13 06:39pascalSummaryunsoundness due to packed struct in r11868 => unsoundness due to packed structs
2011-02-13 06:47pascalNote Added: 0001488
2011-05-02 16:24svn
2011-05-02 16:24svnStatusassigned => resolved
2011-05-02 16:24svnResolutionopen => fixed
2011-10-10 14:13signolesFixed in Version => Frama-C Nitrogen-20111001
2011-10-10 14:14signolesStatusresolved => closed
2013-12-19 01:12svnSource_changeset_attached => framac master 315f9ade
2014-02-12 16:54monateSource_changeset_attached => framac stable/neon 315f9ade
2014-02-12 16:59monateNote Added: 0004799
2014-02-12 16:59monateAssigned Topascal => monate
2014-02-12 16:59monateStatusclosed => resolved