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
  • #630
Closed
Open
Created Jun 12, 2015 by mantis-gitlab-migration@mantis-gitlab-migration

Weak and Strong Invariants are not supported

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


Id Project Category View Due Date Updated
ID0002134 Frama-C Kernel > ACSL implementation public 2015-06-12 2015-06-12
Reporter gaggarwal Assigned To virgile Resolution open
Priority normal Severity minor Reproducibility have not tried
Platform - OS - OS Version -
Product Version Frama-C Neon-20140301 Target Version - Fixed in Version -

Description :

ACSL manual version 1.8, in Figure 2.23 explains grammar of data-invariant and type-invariant. Section 2.11(Data invariants) explains the difference between between strong and weak invariants.

I tried running the example manual have for strong invariant in the same section. But it seems like weak and strong invariants are not supported and ACSL parser is not able to parse the invariants with inv-strength.

Steps To Reproduce :

I used example ACSL manual version 1.8 have :

int a; //@ global invariant a_is_positive: a >= 0 ;

typedef double temperature; /@ strong type invariant temp_in_celsius(temperature t) = @ t >= -273.15 ; @/

struct S { int f; };

//@ type invariant S_f_is_positive(struct S s) = s.f >= 0 ;

Ran "frama-c -wp file.c" command and got following kernel error:

file.c:5:[kernel] user error: unexpected token 'type'

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