Frama-C Bug Tracking System - Frama-C
View Issue Details
0002426Frama-CPlug-in > wppublic2019-02-12 15:552019-02-12 17:19
closedno change required 
LinuxLinux Manjaro
0002426: One \valid seems sufficient to write in a whole array.
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
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.
No tags attached.
Issue History
2019-02-12 15:55VincentPenelleNew Issue
2019-02-12 15:55VincentPenelleStatusnew => assigned
2019-02-12 15:55VincentPenelleAssigned To => correnson
2019-02-12 17:14corrensonNote Added: 0006744
2019-02-12 17:16corrensonNote Added: 0006745
2019-02-12 17:16corrensonStatusassigned => closed
2019-02-12 17:16corrensonResolutionopen => no change required
2019-02-12 17:19corrensonNote Edited: 0006744View Revisions

2019-02-12 17:14   
(edited on: 2019-02-12 17:19)
This is simply because, in memory models of WP, it is not possible to have a memory block with different access conditions. This means that valid-read and valid only depends on the base-address of the pointer, provided the offset is in the range of allocated ones. Hence, If you assume that some pointer p in a block is valid, all pointers in the same block that are valid-read are also valid. Conversely, if you assume that some pointer p in a block is valid-read, then any pointer in the same block is either valid-read or not valid. Actually, the only blocks that are read-only are const globals and string literals. All other blocks have always read-write access.
2019-02-12 17:16   
Post-scriptum : you shall add a loop-assign in your loop, otherwise, all variables (including, a[...], n, and i) might be modified during the loop.