Skip to content
Snippets Groups Projects
Commit 61ce82b2 authored by Loïc Correnson's avatar Loïc Correnson
Browse files

[wp] useless side-behaviors for smoke tests

parent d779872d
No related branches found
No related tags found
No related merge requests found
......@@ -37,11 +37,9 @@ Goal Wp_smoke_default_requires in 'foo':
Assume {
Type: is_sint32(x).
(* Pre-condition *)
Have: (x < 0) /\ P_REQUIRES(0, x).
(* Pre-condition for 'A' *)
Have: (P_ASSUMES(1, x) -> ((3 <= x) /\ P_REQUIRES(1, x))).
(* Pre-condition for 'B' *)
Have: (P_ASSUMES(2, x) -> P_REQUIRES(2, x)).
Have: P_REQUIRES(0, x).
(* Pre-condition *)
Have: x < 0.
}
Prove: false.
......@@ -62,13 +60,13 @@ Goal Wp_smoke_B_requires in 'foo':
Assume {
Type: is_sint32(x).
(* Pre-condition *)
Have: (x < 0) /\ P_REQUIRES(0, x).
(* Pre-condition for 'A' *)
Have: (P_ASSUMES(1, x) -> ((3 <= x) /\ P_REQUIRES(1, x))).
(* Pre-condition for 'B' *)
Have: P_REQUIRES(2, x).
Have: P_REQUIRES(0, x).
(* Pre-condition *)
Have: x < 0.
(* Pre-condition for 'B' *)
Have: P_ASSUMES(2, x).
(* Pre-condition for 'B' *)
Have: P_REQUIRES(2, x).
}
Prove: false.
......
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