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.