Skip to content
GitLab
Projects Groups Topics 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
    • Contributor statistics
    • Graph
    • Compare revisions
  • Issues 168
    • Issues 168
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 0
    • Merge requests 0
  • Deployments
    • Deployments
    • Releases
  • Packages and registries
    • Packages and registries
    • Container Registry
    • Model experiments
  • 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
  • #68

unbound logic variable warning for local variable

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


Id Project Category View Due Date Updated
ID0002500 Frama-C Kernel > ACSL implementation public 2020-03-10 2020-03-20
Reporter jens Assigned To signoles Resolution no change required
Priority high Severity major Reproducibility always
Platform - OS linux, macOS OS Version -
Product Version Frama-C 20-Calcium Target Version - Fixed in Version -

Description :

When processing the following lines

/*@ requires 0 < n; requires \valid(a + (0..n-1)); / void foo(int a, int n) { int m = 0; //@ assert a[m] == \at(a[m],Pre); }

with 'frama-c -wp label_pointer.c ', I obtain the following error message for the assertion.

[kernel] Parsing label_pointer.c (with preprocessing) [kernel:annot-error] label_pointer.c:9: Warning: unbound logic variable m. Ignoring code annotation [kernel] User Error: warning annot-error treated as fatal error. [kernel] User Error: stopping on file "label_pointer.c" that has errors. Add '-kernel-msg-key pp' for preprocessing command. [kernel] Frama-C aborted: invalid user input.

To me this looks like a bug or am I missing something crucial here? (The message does NOT appear when 'Pre' is replaced by 'Here'.)

Attachments

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