Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000830Frama-CKernelpublic2011-05-20 02:592011-10-10 14:14
Reporterhorsh 
Assigned Topascal 
PrioritynormalSeveritycrashReproducibilityalways
StatusclosedResolutionduplicate 
PlatformOSOS Version
Product VersionFrama-C Carbon-20110201 
Target VersionFixed in VersionFrama-C Nitrogen-20111001 
Summary0000830: unsigned :32 bitfield assertion at another location
Description It looks similar to 0000817,but the actual line number of assertion is different. I could not find any public access to source code younger than Carbon-20110201, so can not tell. $ frama-c --version Version: Carbon-20110201 $ cat red3.i typedef struct { unsigned next:32; } state; typedef struct { state sym; } table; table tables; foo ( unsigned start) { start < ( & tables . sym) -> next ; } $ frama-c red3.i [kernel] error occurring when exiting Frama-C: stopping exit procedure. The full backtrace is: Called from file "cil/src/frontc/cabs2cil.ml", line 1683, characters 16-36 Called from file "cil/src/frontc/cabs2cil.ml", line 5554, characters 15-41 Called from file "cil/src/frontc/cabs2cil.ml", line 4864, characters 30-60 Called from file "cil/src/frontc/cabs2cil.ml", line 5837, characters 20-48 Called from file "cil/src/frontc/cabs2cil.ml", line 7431, characters 28-61 Called from file "cil/src/frontc/cabs2cil.ml", line 7336, characters 25-48 Called from file "list.ml", line 74, characters 24-34 Called from file "cil/src/frontc/cabs2cil.ml", line 7325, characters 9-1023 Called from file "cil/src/frontc/cabs2cil.ml", line 7018, characters 14-321 Called from file "cil/src/frontc/cabs2cil.ml", line 7875, characters 12-31 Called from file "list.ml", line 69, characters 12-15 Called from file "cil/src/frontc/cabs2cil.ml", line 7906, characters 2-26 Called from file "cil/src/frontc/frontc.ml", line 43, characters 19-22 Called from file "src/kernel/file.ml", line 698, characters 16-23 Called from file "list.ml", line 74, characters 24-34 Called from file "src/kernel/file.ml", line 695, characters 6-318 Called from file "src/kernel/file.ml", line 1177, characters 12-30 Called from file "src/kernel/file.ml", line 1265, characters 4-27 Called from file "src/kernel/ast.ml", line 59, characters 2-28 Called from file "src/kernel/ast.ml", line 66, characters 53-71 Called from file "queue.ml", line 134, characters 6-20 Called from file "src/kernel/cmdline.ml", line 169, characters 6-23 Unexpected error (File "cil/src/frontc/cabs2cil.ml", line 1662, characters 13-19: Assertion failed).
TagsNo tags attached.
Attached Filespatch file icon bitfields.patch [^] (95,430 bytes) 2011-05-20 10:31 [Show Content]
patch file icon patch-ac-bitfields.patch [^] (540 bytes) 2011-05-20 15:35 [Show Content]

- Relationships
duplicate of 0000817closedmonate r13378, assertion failed with bit-fields 

-  Notes
(0001914)
pascal (reporter)
2011-05-20 10:31

This is indeed the same issue as 817: the snippet works as expected in the development version. The line numbers are different because there have been many bugfixes in the front-end since the 20110201 release, as a result of playing with a random C program generator named Csmith. This also makes it difficult to backport this particular patch. The development version is indeed not publicly available. Only close collaborators who already have a large investment in the tool can justify the work of staying up-to-date with development. If or when you think you should be in the club, contact Benjamin.Monate@cea.fr to discuss the conditions. If this is blocking, you can try to backport the patch yourself. These are the changes that fixed 817, but I can't promise that this patch doesn't rely on other things being fixed first.
(0001915)
pascal (reporter)
2011-05-20 10:53

Actually the patch contains the changes that fixed bug 823, a bug made visible once 817 was fixed.
(0001918)
virgile (developer)
2011-05-20 16:16

Actually bitfield.patch can not be used against Carbon-20110201 release. In particular, it refers to code in cil.ml that has been moved from cabs2cil.ml, were it lied at the time of the release. patch-ac-bitfields.patch backports the fix of issue 817 (but not 823) in Carbon. It is applied in the godi (http://godi.camlcity.org/) package of frama-c.

- Issue History
Date Modified Username Field Change
2011-05-20 02:59 horsh New Issue
2011-05-20 10:31 pascal File Added: bitfields.patch
2011-05-20 10:31 pascal Note Added: 0001914
2011-05-20 10:31 pascal Status new => resolved
2011-05-20 10:31 pascal Resolution open => fixed
2011-05-20 10:31 pascal Assigned To => pascal
2011-05-20 10:53 pascal Note Added: 0001915
2011-05-20 10:53 pascal Status resolved => feedback
2011-05-20 10:53 pascal Resolution fixed => reopened
2011-05-20 10:53 pascal Status feedback => resolved
2011-05-20 10:53 pascal Resolution reopened => fixed
2011-05-20 15:35 virgile File Added: patch-ac-bitfields.patch
2011-05-20 16:16 virgile Note Added: 0001918
2011-05-20 16:16 virgile Status resolved => feedback
2011-05-20 16:16 virgile Resolution fixed => reopened
2011-05-20 16:17 virgile Relationship added duplicate of 0000817
2011-05-20 16:17 virgile Duplicate ID 0 => 817
2011-05-20 16:17 virgile Status feedback => resolved
2011-05-20 16:17 virgile Resolution reopened => duplicate
2011-10-10 14:13 signoles Fixed in Version => Frama-C Nitrogen-20111001
2011-10-10 14:14 signoles Status resolved => closed


Copyright © 2000 - 2020 MantisBT Team
Powered by Mantis Bugtracker