\valid_read and assigns
ID0001360: This issue was created automatically from Mantis Issue 1360. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0001360 | Frama-C | Plug-in > wp | public | 2013-02-08 | 2014-02-12 |
| Reporter | jens | Assigned To | correnson | Resolution | fixed |
| Priority | normal | Severity | major | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Oxygen-20120901 | Target Version | - | Fixed in Version | Frama-C Fluorine-20130401 |
Description :
In the following specification I have deliberately used "\valid_read" instead of of "\valid".
/*@ requires \valid_read(a);
ensures *a == 0;
assigns *a; / void foo(int a) { *a = 0; }
Frama-C/WP verifies this specification and implementation. However, isn't it wrong that 1.) the assigns clause of the specification refers to a memory location that is not "\valid" but only "\valid_read"? 2.) the implementation writes to a memory location that is not "\valid"?