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 209
    • Issues 209
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 1
    • Merge requests 1
  • Deployments
    • Deployments
    • Releases
  • Monitor
    • Monitor
    • Incidents
  • Packages & Registries
    • Packages & Registries
    • Container Registry
  • Analytics
    • Analytics
    • Value stream
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Commits
  • Issue Boards
Collapse sidebar
  • pub
  • frama-c
  • Issues
  • #169

Closed
Open
Created Feb 12, 2019 by mantis-gitlab-migration@mantis-gitlab-migration

One \valid seems sufficient to write in a whole array.

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


Id Project Category View Due Date Updated
ID0002426 Frama-C Plug-in > wp public 2019-02-12 2019-02-12
Reporter VincentPenelle Assigned To correnson Resolution no change required
Priority normal Severity minor Reproducibility always
Platform Linux OS Linux Manjaro OS Version -
Product Version - Target Version - Fixed in Version -

Description :

I am on Chlorine version. When I try to verify the following function with RTE guard enabled, WP succeeds. However, I think it should not, as only the first cell is specified to be valid, the rest is just specified to have valid read.

/*@ requires \valid(a); @ requires \valid_read(a + (0 .. n-1)); @ requires 0 <= n <= INT_MAX; */ void foo(int a, int n){ /@ loop invariant 0 <= i <= n; @ loop invariant \valid(a + (0 .. n-1)); */ for (int i = 0; i<n;i++) a[i] = i; }

Note: that works as well without any loop. It doesn't work if you declare to pointers with different names, and declare one to be \valid and the other to be \valid_read (like in swap function for example). It looks like the loop invariant \valid is simplified to true by Qed.

If that's normal, please explain me why. Thanks,

Vincent Penelle.

Steps To Reproduce :

Specify an array as being \valid_read, and one of its cells to be \valid. Then, try to write in any cell. Generate the RTE guards. WP should succeed to prove that the cells you're writing in are \valid.

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