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 201
    • Issues 201
    • 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
  • #1753
Closed
Open
Created Mar 08, 2011 by mantis-gitlab-migration@mantis-gitlab-migration

Several [invariant] at a program point

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


Id Project Category View Due Date Updated
ID0000750 Frama-C Kernel > ACSL implementation public 2011-03-08 2014-02-12
Reporter Anne Assigned To virgile Resolution open
Priority normal Severity feature Reproducibility always
Platform - OS - OS Version -
Product Version - Target Version - Fixed in Version -

Description :

If we want to put several [invariant] annotations at a program point, we have to have several ACSL comment, else we get : [kernel] user error: Only one code annotation is allowed per comment But with several comments, several program points are created, and it is then difficult to interpret the invariants, because it seems that they have to be considered as a sequence, while we want to see them as a conjunction...

Would it be possible to have several invariants at the same point like it is done for le [loop invariant] ?

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