Skip to content

GitLab

Commit 0749a30c authored by Loïc Correnson's avatar Loïc Correnson
Browse files

[wp] fix post assigns

parent cbe1c519
Hide whitespace changes
Inline Side-by-side
src/plugins/wp/LogicCompiler.ml
View file @ 0749a30c
......@@ -258,6 +258,10 @@ struct
types = [];
}
let has_at_frame frame label =
assert (not (Clabels.is_here label));
LabelMap.mem label frame.labels
let mem_at_frame frame label =
assert (not (Clabels.is_here label));
try LabelMap.find label frame.labels
......
src/plugins/wp/LogicCompiler.mli
View file @ 0749a30c
......@@ -76,6 +76,7 @@ sig
val guards : frame -> pred list
val mem_frame : c_label -> sigma
val has_at_frame : frame -> c_label -> bool
val mem_at_frame : frame -> c_label -> sigma
val set_at_frame : frame -> c_label -> sigma -> unit
......
src/plugins/wp/LogicSemantics.ml
View file @ 0749a30c
......@@ -63,6 +63,7 @@ struct
let mk_frame = C.mk_frame
let in_frame = C.in_frame
let mem_frame = C.mem_frame
let has_at_frame = C.has_at_frame
let mem_at_frame = C.mem_at_frame
let set_at_frame = C.set_at_frame
let mem_at = C.mem_at
......
src/plugins/wp/Sigs.ml
View file @ 0749a30c
......@@ -658,6 +658,9 @@ sig
(** Update a frame with a specific environment for the given label. *)
val set_at_frame : frame -> Clabels.c_label -> sigma -> unit
(** Chek if a frame already has a specific envioronement for the given label. *)
val has_at_frame : frame -> Clabels.c_label -> bool
(** Same as [mem_at_frame] but for the current frame. *)
val mem_frame : Clabels.c_label -> sigma
......
src/plugins/wp/cfgWP.ml
View file @ 0749a30c
......@@ -658,15 +658,20 @@ struct
if Clabels.is_here label then wp else
in_wenv wenv wp
(fun env wp ->
let frame = L.get_frame () in
let s_here = L.current env in
let s_labl = L.mem_frame label in
let pa = Sigma.join s_here s_labl in
let s_frame =
if L.has_at_frame frame label then
L.mem_at_frame frame label
else
(L.set_at_frame frame label s_here ; s_here) in
let pa = Sigma.join s_here s_frame in
let stop,effects = Eset.partition (is_stopeffect label) wp.effects in
let vcs = Gmap.filter (not_posteffect stop) wp.vcs in
let vcs = passify_vcs pa vcs in
let vcs = check_nothing stop vcs in
let vcs = state_vcs stmt s_here vcs in
{ sigma = Some s_here ; vcs=vcs ; effects=effects })
{ sigma = Some s_frame ; vcs=vcs ; effects=effects })
(* -------------------------------------------------------------------------- *)
(* --- WP RULE : assignation --- *)
......@@ -1051,6 +1056,7 @@ struct
let seq_post = cc_havoc dom_call seq_result.pre in
let seq_exit = cc_havoc dom_call (sigma_at wexit) in
(* Pre-State *)
(* Passive: joined later by call_proper *)
let sigma_pre, _, _ = Sigma.merge seq_post.pre seq_exit.pre in
let formals = List.map (C.exp sigma_pre) es in
let call = L.call kf formals in
......
src/plugins/wp/tests/wp_hoare/oracle/dispatch_var2.0.res.oracle
View file @ 0749a30c
......@@ -14,15 +14,20 @@ Assume {
(* Heap *)
Type: is_sint32(x_1).
(* Block In *)
Have: (Init_tmp_0=false) /\ (ta_tmp_0=false).
Have: (Init_tmp_0=false) /\ (ta_tmp_0=true) /\ (ta_tmp_1=false).
Have: ((Init_tmp_0=true) <-> (Init_tmp_1=true)) /\
((ta_tmp_0=true) <-> (ta_tmp_2=true)).
(* Call 'reset' *)
Have: x = 0.
Have: (ta_tmp_2=true) <-> (ta_tmp_3=true).
(* Call 'load' *)
Have: (tmp_0 = load_0) /\ (x = load_0).
(* Return Effects *)
Have: ((Init_tmp_0=true) -> (Init_tmp_1=true)).
Have: ((Init_tmp_1=true) -> (Init_tmp_2=true)).
(* Return *)
Have: tmp_0 = call_global_0.
(* Block Out *)
Have: (ta_tmp_3=true).
}
Prove: call_global_0 = 0.
......@@ -47,12 +52,13 @@ Assume {
Have: (ta_tmp_1=true) <-> (ta_tmp_0=true).
(* Block In *)
Have: (Init_tmp_0=false) /\ (ta_tmp_1=false).
Have: (Init_tmp_0=true) <-> (Init_tmp_1=true).
(* Call 'reset' *)
Have: x = 0.
(* Call 'load' *)
Have: x = load_0.
(* Return Effects *)
Have: ((Init_tmp_0=true) -> (Init_tmp_1=true)).
Have: ((Init_tmp_1=true) -> (Init_tmp_2=true)).
}
Prove: (ta_tmp_0=false).
......@@ -78,19 +84,26 @@ Assume {
Type: is_sint32(call_local_0) /\ is_sint32(load_0) /\ is_sint32(tmp_0) /\
is_sint32(z).
(* Block In *)
Have: (Init_tmp_0=false) /\ (Init_z_0=false) /\ (ta_tmp_0=false) /\
(ta_z_0=false).
Have: (Init_z_0=true) <-> (Init_z_1=true).
Have: (Init_tmp_0=false) /\ (Init_z_0=false) /\ (ta_tmp_0=true) /\
(ta_tmp_1=false) /\ (ta_z_0=true) /\ (ta_z_1=false).
Have: ((Init_tmp_0=true) <-> (Init_tmp_1=true)) /\
((Init_z_0=true) <-> (Init_z_1=true)) /\
((ta_tmp_0=true) <-> (ta_tmp_2=true)) /\
((ta_z_0=true) <-> (ta_z_2=true)).
(* Call 'reset' *)
Have: z = 0.
Have: (ta_z_0=true) /\ (z = 0).
(* Call Effects *)
Have: ((Init_z_1=true) -> (Init_z_2=true)).
Have: ((ta_tmp_2=true) <-> (ta_tmp_3=true)) /\
((ta_z_2=true) <-> (ta_z_3=true)).
(* Call 'load' *)
Have: (tmp_0 = load_0) /\ (z = load_0).
Have: (ta_z_2=true) /\ (tmp_0 = load_0) /\ (z = load_0).
(* Return Effects *)
Have: ((Init_tmp_0=true) -> (Init_tmp_1=true)).
Have: ((Init_tmp_1=true) -> (Init_tmp_2=true)).
(* Return *)
Have: tmp_0 = call_local_0.
(* Block Out *)
Have: (ta_tmp_3=true) /\ (ta_z_3=true).
}
Prove: call_local_0 = 0.
......@@ -107,17 +120,20 @@ Assume {
Type: is_sint32(status_0) /\ is_sint32(status_1) /\ is_sint32(z).
Have: (ta_z_1=true) <-> (ta_z_0=true).
(* Block In *)
Have: (Init_z_0=false) /\ (ta_tmp_0=false) /\ (ta_z_1=false).
Have: (Init_z_0=false) /\ (ta_tmp_0=false) /\ (ta_z_2=true) /\
(ta_z_1=false).
(* Merge *)
Either {
Case:
Have: (Init_z_0=true) <-> (Init_z_1=true).
(* Call 'reset' *)
Have: z = 0.
Have: (ta_z_2=true) /\ (z = 0).
(* Call Effects *)
Have: ((Init_z_1=true) -> (Init_z_2=true)).
Case:
Have: (Init_z_0=true) <-> (Init_z_3=true).
(* Exit 'reset' *)
Have: (ta_z_2=true).
(* Exit Effects *)
Have: ((Init_z_3=true) -> (Init_z_4=true)).
}
......@@ -137,10 +153,11 @@ Assume {
Type: is_sint32(z).
Have: (ta_z_1=true) <-> (ta_z_0=true).
(* Block In *)
Have: (Init_z_0=false) /\ (ta_tmp_0=false) /\ (ta_z_1=false).
Have: (Init_z_0=false) /\ (ta_tmp_0=false) /\ (ta_z_2=true) /\
(ta_z_1=false).
Have: (Init_z_0=true) <-> (Init_z_1=true).
(* Call 'reset' *)
Have: z = 0.
Have: (ta_z_2=true) /\ (z = 0).
(* Call Effects *)
Have: ((Init_z_1=true) -> (Init_z_2=true)).
}
......@@ -155,16 +172,18 @@ Assume {
Have: (ta_tmp_1=true) <-> (ta_tmp_0=true).
(* Block In *)
Have: (Init_tmp_0=false) /\ (Init_z_0=false) /\ (ta_tmp_1=false) /\
(ta_z_0=false).
Have: (Init_z_0=true) <-> (Init_z_1=true).
(ta_z_0=true) /\ (ta_z_1=false).
Have: ((Init_tmp_0=true) <-> (Init_tmp_1=true)) /\
((Init_z_0=true) <-> (Init_z_1=true)) /\
((ta_z_0=true) <-> (ta_z_2=true)).
(* Call 'reset' *)
Have: z = 0.
Have: (ta_z_0=true) /\ (z = 0).
(* Call Effects *)
Have: ((Init_z_1=true) -> (Init_z_2=true)).
(* Call 'load' *)
Have: z = load_0.
Have: (ta_z_2=true) /\ (z = load_0).
(* Return Effects *)
Have: ((Init_tmp_0=true) -> (Init_tmp_1=true)).
Have: ((Init_tmp_1=true) -> (Init_tmp_2=true)).
}
Prove: (ta_tmp_0=false).
......@@ -185,11 +204,12 @@ Goal Instance of 'Pre-condition (file tests/wp_hoare/dispatch_var2.i, line 27) i
Assume {
Type: is_sint32(z).
(* Block In *)
Have: (Init_z_0=false) /\ (ta_tmp_0=false) /\ (ta_z_0=true) /\
(ta_z_1=false).
Have: (Init_z_0=true) <-> (Init_z_1=true).
Have: (Init_z_0=false) /\ (ta_tmp_0=false) /\ (ta_z_1=true) /\
(ta_z_2=false).
Have: ((Init_z_0=true) <-> (Init_z_1=true)) /\
((ta_z_1=true) <-> (ta_z_0=true)).
(* Call 'reset' *)
Have: (ta_z_0=true) /\ (z = 0).
Have: (ta_z_1=true) /\ (z = 0).
(* Call Effects *)
Have: ((Init_z_1=true) -> (Init_z_2=true)).
}
......@@ -209,21 +229,22 @@ Assume {
(* Pre-condition *)
Have: (ta_y_0=true).
(* Frame In *)
Have: (ta_y_1=true) /\ (ta_y_0=false).
Have: (ta_y_0=false).
(* Block In *)
Have: (Init_tmp_0=false) /\ (ta_tmp_0=false).
Have: (ta_y_1=true) <-> (ta_y_2=true).
Have: (Init_tmp_0=false) /\ (ta_tmp_0=true) /\ (ta_tmp_1=false).
Have: ((Init_tmp_0=true) <-> (Init_tmp_1=true)) /\
((ta_tmp_0=true) <-> (ta_tmp_2=true)).
(* Call 'reset' *)
Have: (ta_y_1=true) /\ (y = 0).
Have: (ta_y_2=true) <-> (ta_y_3=true).
Have: y = 0.
Have: (ta_tmp_2=true) <-> (ta_tmp_3=true).
(* Call 'load' *)
Have: (ta_y_2=true) /\ (tmp_0 = load_0) /\ (y = load_0).
Have: (tmp_0 = load_0) /\ (y = load_0).
(* Return Effects *)
Have: ((Init_tmp_0=true) -> (Init_tmp_1=true)).
Have: ((Init_tmp_1=true) -> (Init_tmp_2=true)).
(* Return *)
Have: tmp_0 = call_param_0.
(* Frame Out *)
Have: (ta_y_3=true).
(* Block Out *)
Have: (ta_tmp_3=true).
}
Prove: call_param_0 = 0.
......@@ -244,14 +265,11 @@ Assume {
(* Pre-condition *)
Have: (ta_y_1=true).
(* Frame In *)
Have: (ta_y_2=true) /\ (ta_y_1=false).
Have: (ta_y_1=false).
(* Block In *)
Have: (ta_tmp_0=false).
(* Merge *)
Either {
Case: (* Call 'reset' *) Have: (ta_y_2=true) /\ (y = 0).
Case: (* Exit 'reset' *) Have: (ta_y_2=true).
}
Either { Case: (* Call 'reset' *) Have: y = 0. Case: }
}
Prove: (ta_y_0=false).
......@@ -272,11 +290,11 @@ Assume {
(* Pre-condition *)
Have: (ta_y_1=true).
(* Frame In *)
Have: (ta_y_2=true) /\ (ta_y_1=false).
Have: (ta_y_1=false).
(* Block In *)
Have: (ta_tmp_0=false).
(* Call 'reset' *)
Have: (ta_y_2=true) /\ (y = 0).
Have: y = 0.
}
Prove: (ta_y_0=false).
......@@ -292,16 +310,16 @@ Assume {
(* Pre-condition *)
Have: (ta_y_0=true).
(* Frame In *)
Have: (ta_y_1=true) /\ (ta_y_0=false).
Have: (ta_y_0=false).
(* Block In *)
Have: (Init_tmp_0=false) /\ (ta_tmp_1=false).
Have: (ta_y_1=true) <-> (ta_y_2=true).
Have: (Init_tmp_0=true) <-> (Init_tmp_1=true).
(* Call 'reset' *)
Have: (ta_y_1=true) /\ (y = 0).
Have: y = 0.
(* Call 'load' *)
Have: (ta_y_2=true) /\ (y = load_0).
Have: y = load_0.
(* Return Effects *)
Have: ((Init_tmp_0=true) -> (Init_tmp_1=true)).
Have: ((Init_tmp_1=true) -> (Init_tmp_2=true)).
}
Prove: (ta_tmp_0=false).
......@@ -332,12 +350,11 @@ Assume {
(* Pre-condition *)
Have: (ta_y_1=true).
(* Frame In *)
Have: (ta_y_2=true) /\ (ta_y_1=false).
Have: (ta_y_0=true) /\ (ta_y_1=false).
(* Block In *)
Have: (ta_tmp_0=false).
Have: (ta_y_2=true) <-> (ta_y_0=true).
(* Call 'reset' *)
Have: (ta_y_2=true) /\ (y = 0).
Have: (ta_y_0=true) /\ (y = 0).
}
Prove: (ta_y_0=true).
......@@ -351,15 +368,20 @@ Assume {
Type: is_sint32(call_param_ref_0) /\ is_sint32(load_0) /\ is_sint32(q) /\
is_sint32(tmp_0).
(* Block In *)
Have: (Init_tmp_0=false) /\ (ta_tmp_0=false).
Have: (Init_tmp_0=false) /\ (ta_tmp_0=true) /\ (ta_tmp_1=false).
Have: ((Init_tmp_0=true) <-> (Init_tmp_1=true)) /\
((ta_tmp_0=true) <-> (ta_tmp_2=true)).
(* Call 'reset' *)
Have: q = 0.
Have: (ta_tmp_2=true) <-> (ta_tmp_3=true).
(* Call 'load' *)
Have: (q = load_0) /\ (tmp_0 = load_0).
(* Return Effects *)
Have: ((Init_tmp_0=true) -> (Init_tmp_1=true)).
Have: ((Init_tmp_1=true) -> (Init_tmp_2=true)).
(* Return *)
Have: tmp_0 = call_param_ref_0.
(* Block Out *)
Have: (ta_tmp_3=true).
}
Prove: call_param_ref_0 = 0.
......@@ -382,12 +404,13 @@ Assume {
Have: (ta_tmp_1=true) <-> (ta_tmp_0=true).
(* Block In *)
Have: (Init_tmp_0=false) /\ (ta_tmp_1=false).
Have: (Init_tmp_0=true) <-> (Init_tmp_1=true).
(* Call 'reset' *)
Have: q = 0.
(* Call 'load' *)
Have: q = load_0.
(* Return Effects *)
Have: ((Init_tmp_0=true) -> (Init_tmp_1=true)).
Have: ((Init_tmp_1=true) -> (Init_tmp_2=true)).
}
Prove: (ta_tmp_0=false).
......
src/plugins/wp/tests/wp_plugin/oracle/copy.res.oracle
View file @ 0749a30c
......@@ -151,12 +151,18 @@ Prove: a_3[a_4] = a_2[a_4].
------------------------------------------------------------
Goal Loop assigns (file tests/wp_plugin/copy.i, line 12) (1/2):
Goal Loop assigns (file tests/wp_plugin/copy.i, line 12) (1/3):
Prove: true.
------------------------------------------------------------
Goal Loop assigns (file tests/wp_plugin/copy.i, line 12) (2/2):
Goal Loop assigns (file tests/wp_plugin/copy.i, line 12) (2/3):
Effect at line 14
Prove: true.
------------------------------------------------------------
Goal Loop assigns (file tests/wp_plugin/copy.i, line 12) (3/3):
Effect at line 16
Let a_1 = shift_sint32(a, 0).
Let a_2 = havoc(Mint_undef_0, Mint_0, a_1, n).
......
src/plugins/wp/tests/wp_plugin/oracle/post_assigns.res.oracle
View file @ 0749a30c
......@@ -30,15 +30,7 @@ Prove: true.
Goal Assigns (file tests/wp_plugin/post_assigns.i, line 10) in 'receive' (2/2):
Call Effect at line 14
Assume {
Have: 0 <= size_0.
Type: is_sint32(size_1) /\ is_sint32(size_0).
(* Heap *)
Type: (region(message_0.base) <= 0) /\ linked(Malloc_0).
(* Goal *)
When: !invalid(Malloc_0, shift_sint8(message_0, 0), 1 + size_0).
}
Prove: size_0 <= size_1.
Prove: true.
------------------------------------------------------------
[wp] Warning: Memory model hypotheses for function 'receive':
......
src/plugins/wp/tests/wp_plugin/oracle_qualif/copy.res.oracle
View file @ 0749a30c
......@@ -3,7 +3,7 @@
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] 10 goals scheduled
[wp] 11 goals scheduled
[wp] [Alt-Ergo] Goal typed_copy_ensures : Valid
[wp] [Alt-Ergo] Goal typed_copy_loop_invariant_Copy_preserved : Valid
[wp] [Qed] Goal typed_copy_loop_invariant_Copy_established : Valid
......@@ -12,12 +12,13 @@
[wp] [Alt-Ergo] Goal typed_copy_assert_A : Valid
[wp] [Alt-Ergo] Goal typed_copy_assert_B : Valid
[wp] [Qed] Goal typed_copy_loop_assigns_part1 : Valid
[wp] [Alt-Ergo] Goal typed_copy_loop_assigns_part2 : Valid
[wp] [Qed] Goal typed_copy_loop_assigns_part2 : Valid
[wp] [Alt-Ergo] Goal typed_copy_loop_assigns_part3 : Valid
[wp] [Qed] Goal typed_copy_assigns : Valid
[wp] Proved goals: 10 / 10
Qed: 4
[wp] Proved goals: 11 / 11
Qed: 5
Alt-Ergo: 6
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
copy 4 6 10 100%
copy 5 6 11 100%
------------------------------------------------------------
src/plugins/wp/tests/wp_plugin/oracle_qualif/post_assigns.res.oracle
View file @ 0749a30c
......@@ -8,13 +8,12 @@
[wp] [Qed] Goal typed_receive_assigns_exit_part1 : Valid
[wp] [Qed] Goal typed_receive_assigns_exit_part2 : Valid
[wp] [Qed] Goal typed_receive_assigns_normal_part1 : Valid
[wp] [Alt-Ergo] Goal typed_receive_assigns_normal_part2 : Unsuccess
[wp] Proved goals: 4 / 5
Qed: 4
Alt-Ergo: 0 (unsuccess: 1)
[wp] [Qed] Goal typed_receive_assigns_normal_part2 : Valid
[wp] Proved goals: 5 / 5
Qed: 5
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
receive 4 - 5 80.0%
receive 5 - 5 100%
------------------------------------------------------------
[wp] Warning: Memory model hypotheses for function 'receive':
/*@ behavior typed: requires \separated(&size,message+(..)); */
......
src/plugins/wp/tests/wp_plugin/post_assigns.i
View file @ 0749a30c
......@@ -7,7 +7,7 @@ int size;
/*@
ensures size == n;
assigns size, message[ 0 .. \at(size,Post) ]; // FAILS
assigns size, message[ 0 .. \at(size,Post) ];
*/
void receive(int n,char *message) {
size = n ;
......
src/plugins/wp/tests/wp_typed/oracle/user_init.0.res.oracle
View file @ 0749a30c
......@@ -87,12 +87,18 @@ Prove: true.
------------------------------------------------------------
Goal Loop assigns 'Zone' (1/2):
Goal Loop assigns 'Zone' (1/3):
Prove: true.
------------------------------------------------------------
Goal Loop assigns 'Zone' (2/2):
Goal Loop assigns 'Zone' (2/3):
Effect at line 20
Prove: true.
------------------------------------------------------------
Goal Loop assigns 'Zone' (3/3):
Effect at line 20
Let a_1 = shift_sint32(a, 0).
Let a_2 = shift_sint32(a, i).
......
src/plugins/wp/tests/wp_typed/oracle/user_init.1.res.oracle
View file @ 0749a30c
......@@ -87,12 +87,18 @@ Prove: true.
------------------------------------------------------------
Goal Loop assigns 'Zone' (1/2):
Goal Loop assigns 'Zone' (1/3):
Prove: true.
------------------------------------------------------------
Goal Loop assigns 'Zone' (2/2):
Goal Loop assigns 'Zone' (2/3):
Effect at line 20
Prove: true.
------------------------------------------------------------
Goal Loop assigns 'Zone' (3/3):
Effect at line 20
Let a_1 = shift_sint32(a, 0).
Let a_2 = shift_sint32(a, i).
......
src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.res.oracle
View file @ 0749a30c
......@@ -8,14 +8,15 @@
[wp] [CFG] Goal init_t2_v2_exits : Valid (Unreachable)
[wp] [CFG] Goal init_t2_v3_exits : Valid (Unreachable)
[wp] Warning: Missing RTE guards
[wp] 91 goals scheduled
[wp] 92 goals scheduled
[wp] [Alt-Ergo] Goal typed_init_ensures : Valid
[wp] [Alt-Ergo] Goal typed_init_loop_invariant_Partial_preserved : Valid
[wp] [Qed] Goal typed_init_loop_invariant_Partial_established : Valid
[wp] [Alt-Ergo] Goal typed_init_loop_invariant_Range_preserved : Valid
[wp] [Qed] Goal typed_init_loop_invariant_Range_established : Valid
[wp] [Qed] Goal typed_init_loop_assigns_part1 : Valid
[wp] [Alt-Ergo] Goal typed_init_loop_assigns_part2 : Valid
[wp] [Qed] Goal typed_init_loop_assigns_part2 : Valid
[wp] [Alt-Ergo] Goal typed_init_loop_assigns_part3 : Valid
[wp] [Qed] Goal typed_init_assigns : Valid
[wp] [Qed] Goal typed_init_loop_variant_decrease : Valid
[wp] [Qed] Goal typed_init_loop_variant_positive : Valid
......@@ -100,12 +101,12 @@
[wp] [Qed] Goal typed_init_t2_v3_loop_variant_positive : Valid
[wp] [Alt-Ergo] Goal typed_init_t2_v3_loop_variant_2_decrease : Valid
[wp] [Qed] Goal typed_init_t2_v3_loop_variant_2_positive : Valid
[wp] Proved goals: 91 / 91
Qed: 51
[wp] Proved goals: 92 / 92
Qed: 52
Alt-Ergo: 40
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
init 6 4 10 100%
init 7 4 11 100%
init_t1 6 4 10 100%
init_t2_v1 9 8 17 100%
init_t2_v2 9 8 17 100%
......
src/plugins/wp/tests/wp_usage/oracle/core.0.res.oracle
View file @ 0749a30c
......@@ -18,20 +18,16 @@
Goal Post-condition (file tests/wp_usage/core.i, line 12) in 'f':
Assume {
Type: is_sint32(a) /\ is_sint32(b) /\ is_sint32(c) /\ is_sint32(x) /\
is_sint32(x_1) /\ is_sint32(x_2) /\ is_sint32(x_3) /\ is_sint32(x_4).
is_sint32(x_1) /\ is_sint32(x_2) /\ is_sint32(x_3).
If a != 0
Then { Have: x_4 = x. }
Else { Have: x_4 = x. }
Then { Have: x_3 = x. }
Else { Have: x_3 = x. }
If b != 0
Then { Have: x_4 = x_3. }
Else { Have: x_4 = x_3. }
Then { Have: x_3 = x_2. }
Else { Have: x_3 = x_2. }
If c != 0
Then {
Let x_5 = 1 + x_3.
Have: x_5 = x_1.
Have: (x_2 = x_1) /\ (x_5 = x_2).
}
Else { Have: x_5 = x_1. }
Then { Have: (1 + x_2) = x_1. }
Else { Have: (1 + x_2) = x_1. }
}
Prove: P_OBS(x, x_1).
......
Markdown is supported
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