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

[wp] Update test oracles

parent 430143c1
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
src/plugins/wp/tests/wp_plugin/oracle/dynamic.0.res.oracle
+ 2
− 2
View file @ 2fbb761b
......@@ -23,7 +23,7 @@ Assume {
(* Heap *)
Type: (region(closure_0.base) <= 0) /\ framed(Mptr_0).
(* Pre-condition *)
Have: (a = a_1) \/ ((a = a_2) /\ (abs_int(x) <= 5)).
Have: (a = a_1) \/ ((a = a_2) /\ (IAbs.abs(x) <= 5)).
}
Prove: (a = a_2) \/ (a = a_1).
......@@ -50,7 +50,7 @@ Assume {
(* Heap *)
Type: (region(closure_0.base) <= 0) /\ framed(Mptr_0).
(* Pre-condition *)
Have: abs_int(x) <= 5.
Have: IAbs.abs(x) <= 5.
(* Instance of 'f1' *)
(* Call point f1 f2 *)
Have: Mptr_0[shiftfield_F1_S_f(closure_0)] = global(G_f1_22).
......
src/plugins/wp/tests/wp_plugin/oracle/flash.1.res.oracle
+ 58
− 58
View file @ 2fbb761b
......@@ -19,21 +19,21 @@ Let a_1 = C_RdAt_int(a).
Let a_2 = global(G_b_65).
Let a_3 = C_RdAt_int(a_2).
Let a_4 = C_WrAt_int(a_2).
Let a_5 = ((const(0))[(a) <- (const(0))[a]+1]).
Let a_6 = ((a_5)[(a_2) <- (a_5)[a_2]+1]).
Let a_7 = ((a_6)[(a) <- (a_6)[a]+1]).
Let a_5 = Flash.update(Flash.init, a).
Let a_6 = Flash.update(a_5, a_2).
Let a_7 = Flash.update(a_6, a).
Let x_1 = 1 + RD_time_0.
Let x_2 = 1 + WR_time_0.
Let x_3 = OBSERVER_time_0 - 1.
Let x_4 = RD_time_0 - 1.
Let a_8 = L_RD_current(x_4).
Let x_5 = OBSERVER_time_0 - 2.
Let x_6 = L_RD_value(a, (const(0))[a]).
Let x_7 = x_6 + L_RD_value(a_2, (a_8)[a_2]).
Let x_6 = L_RD_value(a, Flash.get(Flash.init, a)).
Let x_7 = x_6 + L_RD_value(a_2, Flash.get(a_8, a_2)).
Let x_8 = RD_time_0 - 2.
Let x_9 = OBSERVER_time_0 - 3.
Let x_10 = L_RD_value(a_2, (a_5)[a_2]).
Let x_11 = L_RD_value(a, (a_6)[a]).
Let x_10 = L_RD_value(a_2, Flash.get(a_5, a_2)).
Let x_11 = L_RD_value(a, Flash.get(a_6, a)).
Assume {
Type: is_sint32(OBSERVER_time_0) /\ is_sint32(RD_time_0) /\
is_sint32(WR_time_0) /\ is_sint32(x_9) /\ is_sint32(x_5) /\
......@@ -44,22 +44,22 @@ Assume {
(* Pre-condition *)
Have: L_OBSERVER(x_9) = nil.
(* Pre-condition *)
Have: L_RD_current(x_8) = const(0).
Have: L_RD_current(x_8) = Flash.init.
(* Pre-condition *)
Have: L_WR_current(WR_time_0) = const(0).
Have: L_WR_current(WR_time_0) = Flash.init.
(* Call 'RD' *)
Have: (a_8 = a_5) /\ (L_OBSERVER(x_5) = [ a_1 ]) /\
(x_7 = L_WR_value(a_2, (const(0))[a_2])).
(x_7 = L_WR_value(a_2, Flash.get(Flash.init, a_2))).
(* Call 'RD' *)
Have: (a_6 = L_RD_current(RD_time_0)) /\ (L_OBSERVER(x_3) = [ a_1, a_3 ]).
(* Call 'WR' *)
Have: (L_WR_current(x_2) = ((const(0))[(a_2) <- (const(0))[a_2]+1])) /\
Have: (L_WR_current(x_2) = Flash.update(Flash.init, a_2)) /\
(L_OBSERVER(OBSERVER_time_0) = [ a_1, a_3, a_4 ]).
(* Call 'RD' *)
Have: (L_OBSERVER(x) = [ a_1, a_3, a_4, a_1 ]) /\
(a_7 = L_RD_current(x_1)).
}
Prove: (a_7)[a] = 2.
Prove: Flash.get(a_7, a) = 2.
------------------------------------------------------------
......@@ -70,21 +70,21 @@ Let a_1 = C_RdAt_int(a).
Let a_2 = global(G_b_65).
Let a_3 = C_RdAt_int(a_2).
Let a_4 = C_WrAt_int(a_2).
Let a_5 = ((const(0))[(a) <- (const(0))[a]+1]).
Let a_6 = ((a_5)[(a_2) <- (a_5)[a_2]+1]).
Let a_7 = ((a_6)[(a) <- (a_6)[a]+1]).
Let a_5 = Flash.update(Flash.init, a).
Let a_6 = Flash.update(a_5, a_2).
Let a_7 = Flash.update(a_6, a).
Let x_1 = 1 + RD_time_0.
Let x_2 = 1 + WR_time_0.
Let x_3 = OBSERVER_time_0 - 1.
Let x_4 = RD_time_0 - 1.
Let a_8 = L_RD_current(x_4).
Let x_5 = OBSERVER_time_0 - 2.
Let x_6 = L_RD_value(a, (const(0))[a]).
Let x_7 = x_6 + L_RD_value(a_2, (a_8)[a_2]).
Let x_6 = L_RD_value(a, Flash.get(Flash.init, a)).
Let x_7 = x_6 + L_RD_value(a_2, Flash.get(a_8, a_2)).
Let x_8 = RD_time_0 - 2.
Let x_9 = OBSERVER_time_0 - 3.
Let x_10 = L_RD_value(a_2, (a_5)[a_2]).
Let x_11 = L_RD_value(a, (a_6)[a]).
Let x_10 = L_RD_value(a_2, Flash.get(a_5, a_2)).
Let x_11 = L_RD_value(a, Flash.get(a_6, a)).
Assume {
Type: is_sint32(OBSERVER_time_0) /\ is_sint32(RD_time_0) /\
is_sint32(WR_time_0) /\ is_sint32(x_9) /\ is_sint32(x_5) /\
......@@ -95,22 +95,22 @@ Assume {
(* Pre-condition *)
Have: L_OBSERVER(x_9) = nil.
(* Pre-condition *)
Have: L_RD_current(x_8) = const(0).
Have: L_RD_current(x_8) = Flash.init.
(* Pre-condition *)
Have: L_WR_current(WR_time_0) = const(0).
Have: L_WR_current(WR_time_0) = Flash.init.
(* Call 'RD' *)
Have: (a_8 = a_5) /\ (L_OBSERVER(x_5) = [ a_1 ]) /\
(x_7 = L_WR_value(a_2, (const(0))[a_2])).
(x_7 = L_WR_value(a_2, Flash.get(Flash.init, a_2))).
(* Call 'RD' *)
Have: (a_6 = L_RD_current(RD_time_0)) /\ (L_OBSERVER(x_3) = [ a_1, a_3 ]).
(* Call 'WR' *)
Have: (L_WR_current(x_2) = ((const(0))[(a_2) <- (const(0))[a_2]+1])) /\
Have: (L_WR_current(x_2) = Flash.update(Flash.init, a_2)) /\
(L_OBSERVER(OBSERVER_time_0) = [ a_1, a_3, a_4 ]).
(* Call 'RD' *)
Have: (L_OBSERVER(x) = [ a_1, a_3, a_4, a_1 ]) /\
(a_7 = L_RD_current(x_1)).
}
Prove: (a_7)[a_2] = 1.
Prove: Flash.get(a_7, a_2) = 1.
------------------------------------------------------------
......@@ -121,21 +121,21 @@ Let a_1 = C_RdAt_int(a).
Let a_2 = global(G_b_65).
Let a_3 = C_RdAt_int(a_2).
Let a_4 = C_WrAt_int(a_2).
Let a_5 = ((const(0))[(a) <- (const(0))[a]+1]).
Let a_6 = ((a_5)[(a_2) <- (a_5)[a_2]+1]).
Let a_5 = Flash.update(Flash.init, a).
Let a_6 = Flash.update(a_5, a_2).
Let x_1 = 1 + WR_time_0.
Let a_7 = ((const(0))[(a_2) <- (const(0))[a_2]+1]).
Let a_7 = Flash.update(Flash.init, a_2).
Let x_2 = RD_time_0 - 1.
Let x_3 = OBSERVER_time_0 - 1.
Let x_4 = RD_time_0 - 2.
Let a_8 = L_RD_current(x_4).
Let x_5 = OBSERVER_time_0 - 2.
Let x_6 = L_RD_value(a, (const(0))[a]).
Let x_7 = x_6 + L_RD_value(a_2, (a_8)[a_2]).
Let x_6 = L_RD_value(a, Flash.get(Flash.init, a)).
Let x_7 = x_6 + L_RD_value(a_2, Flash.get(a_8, a_2)).
Let x_8 = RD_time_0 - 3.
Let x_9 = OBSERVER_time_0 - 3.
Let x_10 = L_RD_value(a_2, (a_5)[a_2]).
Let x_11 = L_RD_value(a, (a_6)[a]).
Let x_10 = L_RD_value(a_2, Flash.get(a_5, a_2)).
Let x_11 = L_RD_value(a, Flash.get(a_6, a)).
Assume {
Type: is_sint32(OBSERVER_time_0) /\ is_sint32(RD_time_0) /\
is_sint32(WR_time_0) /\ is_sint32(x_9) /\ is_sint32(x_8) /\
......@@ -145,12 +145,12 @@ Assume {
(* Pre-condition *)
Have: L_OBSERVER(x_9) = nil.
(* Pre-condition *)
Have: L_RD_current(x_8) = const(0).
Have: L_RD_current(x_8) = Flash.init.
(* Pre-condition *)
Have: L_WR_current(WR_time_0) = const(0).
Have: L_WR_current(WR_time_0) = Flash.init.
(* Call 'RD' *)
Have: (a_8 = a_5) /\ (L_OBSERVER(x_5) = [ a_1 ]) /\
(x_7 = L_WR_value(a_2, (const(0))[a_2])).
(x_7 = L_WR_value(a_2, Flash.get(Flash.init, a_2))).
(* Call 'RD' *)
Have: (a_6 = L_RD_current(x_2)) /\ (L_OBSERVER(x_3) = [ a_1, a_3 ]).
(* Call 'WR' *)
......@@ -158,9 +158,9 @@ Assume {
(L_OBSERVER(OBSERVER_time_0) = [ a_1, a_3, a_4 ]).
(* Call 'RD' *)
Have: (L_OBSERVER(x) = [ a_1, a_3, a_4, a_1 ]) /\
(((a_6)[(a) <- (a_6)[a]+1]) = L_RD_current(RD_time_0)).
(Flash.update(a_6, a) = L_RD_current(RD_time_0)).
}
Prove: (a_7)[a_2] = 1.
Prove: Flash.get(a_7, a_2) = 1.
------------------------------------------------------------
......@@ -171,20 +171,20 @@ Let a_1 = C_RdAt_int(a).
Let a_2 = global(G_b_65).
Let a_3 = C_RdAt_int(a_2).
Let a_4 = C_WrAt_int(a_2).
Let a_5 = ((const(0))[(a) <- (const(0))[a]+1]).
Let a_6 = ((a_5)[(a_2) <- (a_5)[a_2]+1]).
Let a_5 = Flash.update(Flash.init, a).
Let a_6 = Flash.update(a_5, a_2).
Let x_1 = 1 + WR_time_0.
Let x_2 = RD_time_0 - 1.
Let x_3 = OBSERVER_time_0 - 1.
Let x_4 = RD_time_0 - 2.
Let a_7 = L_RD_current(x_4).
Let x_5 = OBSERVER_time_0 - 2.
Let x_6 = L_RD_value(a, (const(0))[a]).
Let x_7 = x_6 + L_RD_value(a_2, (a_7)[a_2]).
Let x_6 = L_RD_value(a, Flash.get(Flash.init, a)).
Let x_7 = x_6 + L_RD_value(a_2, Flash.get(a_7, a_2)).
Let x_8 = RD_time_0 - 3.
Let x_9 = OBSERVER_time_0 - 3.
Let x_10 = L_RD_value(a_2, (a_5)[a_2]).
Let x_11 = L_RD_value(a, (a_6)[a]).
Let x_10 = L_RD_value(a_2, Flash.get(a_5, a_2)).
Let x_11 = L_RD_value(a, Flash.get(a_6, a)).
Let x_12 = x_6 + x_10 + x_11.
Assume {
Type: is_sint32(OBSERVER_time_0) /\ is_sint32(RD_time_0) /\
......@@ -195,20 +195,20 @@ Assume {
(* Pre-condition *)
Have: L_OBSERVER(x_9) = nil.
(* Pre-condition *)
Have: L_RD_current(x_8) = const(0).
Have: L_RD_current(x_8) = Flash.init.
(* Pre-condition *)
Have: L_WR_current(WR_time_0) = const(0).
Have: L_WR_current(WR_time_0) = Flash.init.
(* Call 'RD' *)
Have: (a_7 = a_5) /\ (L_OBSERVER(x_5) = [ a_1 ]) /\
(x_7 = L_WR_value(a_2, (const(0))[a_2])).
(x_7 = L_WR_value(a_2, Flash.get(Flash.init, a_2))).
(* Call 'RD' *)
Have: (a_6 = L_RD_current(x_2)) /\ (L_OBSERVER(x_3) = [ a_1, a_3 ]).
(* Call 'WR' *)
Have: (L_WR_current(x_1) = ((const(0))[(a_2) <- (const(0))[a_2]+1])) /\
Have: (L_WR_current(x_1) = Flash.update(Flash.init, a_2)) /\
(L_OBSERVER(OBSERVER_time_0) = [ a_1, a_3, a_4 ]).
(* Call 'RD' *)
Have: (L_OBSERVER(x) = [ a_1, a_3, a_4, a_1 ]) /\
(((a_6)[(a) <- (a_6)[a]+1]) = L_RD_current(RD_time_0)).
(Flash.update(a_6, a) = L_RD_current(RD_time_0)).
}
Prove: x_12 = (L_RD_value(a, 0) + L_RD_value(a, 1) + L_RD_value(a_2, 0)).
......@@ -221,20 +221,20 @@ Let a_1 = C_RdAt_int(a).
Let a_2 = global(G_b_65).
Let a_3 = C_RdAt_int(a_2).
Let a_4 = C_WrAt_int(a_2).
Let a_5 = ((const(0))[(a) <- (const(0))[a]+1]).
Let a_6 = ((a_5)[(a_2) <- (a_5)[a_2]+1]).
Let a_5 = Flash.update(Flash.init, a).
Let a_6 = Flash.update(a_5, a_2).
Let x_1 = 1 + WR_time_0.
Let x_2 = RD_time_0 - 1.
Let x_3 = OBSERVER_time_0 - 1.
Let x_4 = RD_time_0 - 2.
Let a_7 = L_RD_current(x_4).
Let x_5 = OBSERVER_time_0 - 2.
Let x_6 = L_RD_value(a, (const(0))[a]).
Let x_7 = x_6 + L_RD_value(a_2, (a_7)[a_2]).
Let x_6 = L_RD_value(a, Flash.get(Flash.init, a)).
Let x_7 = x_6 + L_RD_value(a_2, Flash.get(a_7, a_2)).
Let x_8 = RD_time_0 - 3.
Let x_9 = OBSERVER_time_0 - 3.
Let x_10 = L_RD_value(a_2, (a_5)[a_2]).
Let x_11 = L_RD_value(a, (a_6)[a]).
Let x_10 = L_RD_value(a_2, Flash.get(a_5, a_2)).
Let x_11 = L_RD_value(a, Flash.get(a_6, a)).
Assume {
Type: is_sint32(OBSERVER_time_0) /\ is_sint32(RD_time_0) /\
is_sint32(WR_time_0) /\ is_sint32(x_9) /\ is_sint32(x_8) /\
......@@ -244,20 +244,20 @@ Assume {
(* Pre-condition *)
Have: L_OBSERVER(x_9) = nil.
(* Pre-condition *)
Have: L_RD_current(x_8) = const(0).
Have: L_RD_current(x_8) = Flash.init.
(* Pre-condition *)
Have: L_WR_current(WR_time_0) = const(0).
Have: L_WR_current(WR_time_0) = Flash.init.
(* Call 'RD' *)
Have: (a_7 = a_5) /\ (L_OBSERVER(x_5) = [ a_1 ]) /\
(x_7 = L_WR_value(a_2, (const(0))[a_2])).
(x_7 = L_WR_value(a_2, Flash.get(Flash.init, a_2))).
(* Call 'RD' *)
Have: (a_6 = L_RD_current(x_2)) /\ (L_OBSERVER(x_3) = [ a_1, a_3 ]).
(* Call 'WR' *)
Have: (L_WR_current(x_1) = ((const(0))[(a_2) <- (const(0))[a_2]+1])) /\
Have: (L_WR_current(x_1) = Flash.update(Flash.init, a_2)) /\
(L_OBSERVER(OBSERVER_time_0) = [ a_1, a_3, a_4 ]).
(* Call 'RD' *)
Have: (L_OBSERVER(x) = [ a_1, a_3, a_4, a_1 ]) /\
(((a_6)[(a) <- (a_6)[a]+1]) = L_RD_current(RD_time_0)).
(Flash.update(a_6, a) = L_RD_current(RD_time_0)).
}
Prove: (L_RD_value(a, 0) + L_RD_value(a_2, 0)) = L_WR_value(a_2, 0).
......
src/plugins/wp/tests/wp_plugin/oracle/float_real.0.res.oracle
+ 1
− 1
View file @ 2fbb761b
......@@ -20,6 +20,6 @@ Assume {
}
Else { Have: dequal_0 = 0. }
}
Prove: (abs_real(x - y) < (1.0/100000)) <-> (dequal_0 != 0).
Prove: (RAbs.abs(x - y) < (1.0/100000)) <-> (dequal_0 != 0).
------------------------------------------------------------
src/plugins/wp/tests/wp_plugin/oracle/float_real.1.res.oracle
+ 1
− 1
View file @ 2fbb761b
......@@ -22,6 +22,6 @@ Assume {
}
Else { Have: dequal_0 = 0. }
}
Prove: (abs_real(of_f64(x) - of_f64(y)) < (1.0/100000)) <-> (dequal_0 != 0).
Prove: (RAbs.abs(of_f64(x) - of_f64(y)) < (1.0/100000)) <-> (dequal_0 != 0).
------------------------------------------------------------
src/plugins/wp/tests/wp_plugin/oracle/math.res.oracle
+ 1
− 1
View file @ 2fbb761b
......@@ -231,7 +231,7 @@ Prove: exp(log(r)) = r.
------------------------------------------------------------
Goal Post-condition 'min_plus_distrib' in 'ok':
Prove: (r + min_real(r_1, r_2)) = min_real(r_1 + r, r_2 + r).
Prove: (r + Rg.min(r_1, r_2)) = Rg.min(r_1 + r, r_2 + r).
------------------------------------------------------------
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment