Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002426Frama-CPlug-in > wppublic2019-02-12 15:552019-02-12 17:19
ReporterVincentPenelle 
Assigned Tocorrenson 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionno change required 
PlatformLinuxOSLinux ManjaroOS Version
Product Version 
Target VersionFixed in Version 
Summary0002426: One \valid seems sufficient to write in a whole array.
DescriptionI 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 ReproduceSpecify 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.
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0006744)
correnson (manager)
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.

(0006745)
correnson (manager)
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.

- Issue History
Date Modified Username Field Change
2019-02-12 15:55 VincentPenelle New Issue
2019-02-12 15:55 VincentPenelle Status new => assigned
2019-02-12 15:55 VincentPenelle Assigned To => correnson
2019-02-12 17:14 correnson Note Added: 0006744
2019-02-12 17:16 correnson Note Added: 0006745
2019-02-12 17:16 correnson Status assigned => closed
2019-02-12 17:16 correnson Resolution open => no change required
2019-02-12 17:19 correnson Note Edited: 0006744 View Revisions


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker