Skip to content
Snippets Groups Projects
Commit b9db0c62 authored by Allan Blanchard's avatar Allan Blanchard
Browse files

[wp] Update test oracle

parent e57aab69
No related branches found
No related tags found
No related merge requests found
...@@ -17,13 +17,15 @@ Prove: true. ...@@ -17,13 +17,15 @@ Prove: true.
------------------------------------------------------------ ------------------------------------------------------------
Goal Post-condition (file tests/wp_acsl/base_offset.i, line 15) in 'f': Goal Post-condition (file tests/wp_acsl/base_offset.i, line 15) in 'f':
Let x = p.offset. Let x = p.base.
Let x_1 = base_offset_table(x).
Let x_2 = p.offset.
Assume { Assume {
(* Heap *) (* Heap *)
Type: region(p.base) <= 0. Type: region(x) <= 0.
(* Goal *) (* Goal *)
When: (0 <= i) /\ (i <= i_1) /\ (i_1 <= 3). When: (0 <= i) /\ (i <= i_1) /\ (i_1 <= 3).
} }
Prove: base_offset(1 + i + x) <= base_offset(1 + i_1 + x). Prove: base_offset(x_1, 1 + i + x_2) <= base_offset(x_1, 1 + i_1 + x_2).
------------------------------------------------------------ ------------------------------------------------------------
...@@ -5,11 +5,11 @@ ...@@ -5,11 +5,11 @@
[wp] 3 goals scheduled [wp] 3 goals scheduled
[wp] [Qed] Goal typed_f_ensures : Valid [wp] [Qed] Goal typed_f_ensures : Valid
[wp] [Qed] Goal typed_f_ensures_2 : Valid [wp] [Qed] Goal typed_f_ensures_2 : Valid
[wp] [Alt-Ergo] Goal typed_f_ensures_3 : Unsuccess [wp] [Alt-Ergo] Goal typed_f_ensures_3 : Valid
[wp] Proved goals: 2 / 3 [wp] Proved goals: 3 / 3
Qed: 2 Qed: 2
Alt-Ergo: 0 (unsuccess: 1) Alt-Ergo: 1
------------------------------------------------------------ ------------------------------------------------------------
Functions WP Alt-Ergo Total Success Functions WP Alt-Ergo Total Success
f 2 - 3 66.7% f 2 1 3 100%
------------------------------------------------------------ ------------------------------------------------------------
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment