Check that all occurrences of *p in assigns are guarded by a \valid(p) in requires
ID0001761: This issue was created automatically from Mantis Issue 1761. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0001761 | Frama-C | Kernel > ACSL implementation | public | 2014-04-23 | 2017-03-14 |
| Reporter | jens | Assigned To | virgile | Resolution | open |
| Priority | normal | Severity | major | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Neon-20140301 | Target Version | - | Fixed in Version | - |
Description :
Here is a simple function foo where the assigns clause refers to the pointer a+n that is not guarded by a \valid in the requires clause.
/@ requires \valid(a + (0..n-1)); assigns a[0..n]; // should be a[0..n-1] / void foo(int a, unsigned int n) { /@ loop invariant 0 <= i <= n; loop assigns i, a[0..n]; // should be a[0..n-1]; loop variant n-i; */ for(unsigned int i = 0; i < n; ++i) a[i] = 0; }
Using the command line
frama-c-gui.byte -wp -wp-rte -wp-model Typed+ref -wp-timeout 10 -wp-prover alt-ergo -wp-out loop_assigns.wp loop_assigns.cI can see that all proof obligations are discharged by either Qed or Alt-Ergo.
My question is about the assigns clause which refers to all offsets of a in the range [0..n]. (Note that I use the same range in the loop assigns clause.) The precondition, however, only states that array offsets in the range [0..n-1] are valid. I think I would prefer if WP (or the Frama-C kernel) issued a warning about this discrepancy.
Additional Information :
I posted this on the Frama-C mailing list. As far as I understood the discussion there it might be a feature request for the Frama-C kernel.
I noticed this problem when writing specs for code from a partner in the OpenETCS project.