Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000525Frama-CKernelpublic2010-06-30 16:522010-12-17 19:36
Reportersduprat 
Assigned Tovirgile 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Beryllium-20090902 
Target VersionFixed in VersionFrama-C Carbon-20101201-beta1 
Summary0000525: inchoherence of types between enumitems and enum type with multi-files
DescriptionWhen a same type definition of enum is used in several files, but in different order, the type of the enumitem is desynchronised with the enum type.
Additional InformationIn the following case (see archive files), the output of the demonstrator plugin indicates that :

exp p1 of type enum __anonenum_T_EN1_1
exp E1 of type enum __anonenum_T_EN1_2

So, this prevent us of comparing both types to check their compatibility.
The enumitem is always in the form of __anonenum_<type>.
The var is of Tname type refering to an other anonenum type.

If we reorder the type declarations in source1, the problem will disappear.
There is no problem with just one file at a time.

scripts
  - build the plugin (make all install)
  - run "frama-c -test1 source1.c source2.c"

[virgile-20100701]
note: the test1.ml in the archive will not compile against current svn. Use the one provided separately instead
TagsNo tags attached.
Attached Filesgz file icon enums.tar.gz [^] (102,070 bytes) 2010-06-30 16:52
? file icon test1.ml [^] (800 bytes) 2010-07-01 10:47 [Show Content]

- Relationships

-  Notes
There are no notes attached to this issue.

- Issue History
Date Modified Username Field Change
2010-06-30 16:52 sduprat New Issue
2010-06-30 16:52 sduprat File Added: enums.tar.gz
2010-07-01 10:46 virgile Status new => assigned
2010-07-01 10:46 virgile Assigned To => virgile
2010-07-01 10:46 virgile Status assigned => acknowledged
2010-07-01 10:47 virgile File Added: test1.ml
2010-07-01 10:48 virgile Additional Information Updated
2010-07-01 14:21 svn Checkin
2010-07-01 14:21 svn Status acknowledged => resolved
2010-07-01 14:21 svn Resolution open => fixed
2010-12-10 15:45 signoles Fixed in Version => Frama-C Carbon-20101201-beta1
2010-12-17 19:36 signoles Status resolved => closed


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker