Frama-C Bug Tracking System
Main | My View | View Issues | Change Log | Roadmap | Repositories
  

View Issue Details [ Jump to Notes ] [ Related Changesets ] [ Issue History ] [ Print ]
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.
Attached Filesc file icon foo_pp.c [^] (54,091 bytes) 2011-02-13 05:47 [Show Content]

- Relationships

-  Notes
(0001488)
pascal (reporter)
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 (reporter)
2014-02-12 16:59

 Fix committed to stable/neon branch.

- Issue History
Date Modified Username Field Change
2011-02-13 05:47 regehr New Issue
2011-02-13 05:47 regehr Status new => assigned
2011-02-13 05:47 regehr Assigned To => pascal
2011-02-13 05:47 regehr File Added: foo_pp.c
2011-02-13 06:39 pascal Category Plug-in > value analysis => Kernel
2011-02-13 06:39 pascal Product Version Frama-C GIT, precise the release id => Frama-C Carbon-20110201
2011-02-13 06:39 pascal Summary unsoundness due to packed struct in r11868 => unsoundness due to packed structs
2011-02-13 06:47 pascal Note Added: 0001488
2011-05-02 16:24 svn Checkin
2011-05-02 16:24 svn Status assigned => resolved
2011-05-02 16:24 svn Resolution open => fixed
2011-10-10 14:13 signoles Fixed in Version => Frama-C Nitrogen-20111001
2011-10-10 14:14 signoles Status resolved => closed
2014-02-12 16:59 monate Note Added: 0004799
2014-02-12 16:59 monate Assigned To pascal => monate
2014-02-12 16:59 monate Status closed => resolved

Copyright © 2000 - 2017 MantisBT Team
Powered by Mantis Bugtracker