requires in beahviors do not behave as expected
ID0002133: This issue was created automatically from Mantis Issue 2133. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0002133 | Frama-C | Plug-in > wp | public | 2015-06-12 | 2015-06-29 |
| Reporter | DavidCok | Assigned To | correnson | Resolution | won't fix |
| Priority | normal | Severity | major | Reproducibility | always |
| Platform | - | OS | Windows | OS Version | 7 |
| Product Version | Frama-C Neon-20140301 | Target Version | - | Fixed in Version | - |
Description :
See the code below. The second case proves the assignment temp=p[0] OK, the first case does not (with -wp-rte enabled), using Frama-C with default alt-ergo. The corresponding proof obligations are shown below the code. The difference between the two cases is that the requires clause is pulled out in front in the second case.
The proof in the second case includes as an assumption the stated requires clause. And it proves OK even if the requires clause is requires (num == 2) ==> (\valid(p) && \valid(p+1));
However the first proof has no assumptions corresponding to the requires clause.
This appears to me to be a bug in WP but the language of the proof obligations is unfamiliar to me - so I'd be glad to have this case explained.
/*@ @ @ behavior b2: @ assumes num == 2; @ requires \valid(p) && \valid(p+1); @ ensures p[1] == \old(p[0]) && p[0] == \old(p[1]); */
void swap(int* p, int num) { int temp; switch (num) { case 2: temp = p[0]; p[0] = p[1]; p[1] = temp; break; default: } }
/*@ @ requires \valid(p) && \valid(p+1); @ behavior b2: @ assumes num == 2; @ ensures p[1] == \old(p[0]) && p[0] == \old(p[1]); */
void swap2(int* p, int num) { int temp; switch (num) { case 2: temp = p[0]; p[0] = p[1]; p[1] = temp; break; default: } }
FramacWp: Function swap
FramacWp: ------------------------------------------------------------
FramacWp:
FramacWp: Goal Assertion 'rte,mem_access' (file C/cygwin/home/sb/trunk/nasa-speedy/EditorTest/src/behaviorBug.c, line 14):
FramacWp: Tags: Case 2.
FramacWp: Assume { (* Heap *) Have: (linked Malloc_0). }
FramacWp: Prove: (valid_rd Malloc_0 (shift p_1 0) 1).
FramacWp: Prover Alt-Ergo returns Unknown (1s)
FramacWp:
FramacWp: ------------------------------------------------------------
FramacWp: Function swap2
FramacWp: ------------------------------------------------------------
FramacWp:
FramacWp: Goal Assertion 'rte,mem_access' (file C/cygwin/home/sb/trunk/nasa-speedy/EditorTest/src/behaviorBug.c, line 33):
FramacWp: Tags: Case 2.
FramacWp: Assume {
FramacWp: (* Heap )
FramacWp: Have: (linked Malloc_0).
FramacWp: ( Pre-condition (file C/cygwin/home/sb/trunk/nasa-speedy/EditorTest/src/behaviorBug.c, line 24) in 'swap2' )
FramacWp: ( Pre-condition: *)
FramacWp: Have: (valid_rw Malloc_0 p_1 1) /\ (valid_rw Malloc_0 (shift p_1 1) 1).
FramacWp: }
FramacWp: Prove: (valid_rd Malloc_0 (shift p_1 0) 1).
FramacWp: Prover Alt-Ergo returns Valid (16)