2021-03-02 02:36 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0000525Frama-CKernelpublic2010-12-17 19:36
Assigned Tovirgile 
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.

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

note: the test1.ml in the archive will not compile against current svn. Use the one provided separately instead
TagsNo tags attached.
Attached Files
  • gz file icon enums.tar.gz (102,070 bytes) 2010-06-30 16:52
  • ? file icon test1.ml (800 bytes) 2010-07-01 10:47 -
    module Self =
           let name = "Test Enum functions"
           let shortname = "test1"
           let module_name = "TestEnum.Self"
           let descr = "Test Enum functions"
           let is_dynamic = true
    module Enabled = Self.False
         let module_name = "TestEnum.Enabled"
         let option_name = "-test1"
         let descr = "Do the Test enum"
         let kind = `Irrelevant
    open Cabs
    let startup _ =
      if Enabled.get () then
        let v = object
          inherit Visitor.frama_c_inplace as super
          method vexpr e =
    	Format.printf "exp %a of type %a\n" !Ast_printer.d_exp e !Ast_printer.d_type (Cil.unrollType (Cil.typeOf e));
          Visitor.visitFramacFileSameGlobals v (Ast.get ())
    let () =
      Db.Main.extend startup
    ? file icon test1.ml (800 bytes) 2010-07-01 10:47 +


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
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
+Issue History