Skip to content

GitLab

  • Menu
Projects Groups Snippets
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in
  • F frama-c
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 204
    • Issues 204
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 0
    • Merge requests 0
  • Deployments
    • Deployments
    • Releases
  • Packages & Registries
    • Packages & Registries
    • Container Registry
  • Monitor
    • Monitor
    • Incidents
  • Analytics
    • Analytics
    • Value stream
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Commits
  • Issue Boards
Collapse sidebar
  • pub
  • frama-c
  • Issues
  • #2296
Closed
Open
Created Jun 30, 2010 by Stephane Duprat@sduprat

inchoherence of types between enumitems and enum type with multi-files

ID0000525: This issue was created automatically from Mantis Issue 525. Further discussion may take place here.


Id Project Category View Due Date Updated
ID0000525 Frama-C Kernel public 2010-06-30 2010-12-17
Reporter sduprat Assigned To virgile Resolution fixed
Priority normal Severity minor Reproducibility always
Platform - OS - OS Version -
Product Version Frama-C Beryllium-20090902 Target Version - Fixed in Version Frama-C Carbon-20101201-beta1

Description :

When 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 Information :

In 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. 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

Attachments

  • enums.tar.gz
  • test1.ml
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking