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

[wp] pre-conditions naming

parent 7da8f87b
No related branches found
No related tags found
No related merge requests found
...@@ -165,7 +165,7 @@ Assume { ...@@ -165,7 +165,7 @@ Assume {
is_sint32(x_4) /\ is_sint32(x_5) /\ is_sint32(x_6) /\ is_sint32(x_7). is_sint32(x_4) /\ is_sint32(x_5) /\ is_sint32(x_6) /\ is_sint32(x_7).
(* Heap *) (* Heap *)
Type: (region(a.base) <= 0) /\ (region(r.base) <= 0). Type: (region(a.base) <= 0) /\ (region(r.base) <= 0).
(* Pre-condition *) (* Pre-condition 'KO' *)
Have: P_OBS(x, x_1, x_2). Have: P_OBS(x, x_1, x_2).
} }
Prove: P_OBS(x_5, x_6, x_7). Prove: P_OBS(x_5, x_6, x_7).
......
...@@ -62,7 +62,7 @@ Let x_4 = x + x_1. ...@@ -62,7 +62,7 @@ Let x_4 = x + x_1.
Assume { Assume {
Type: is_sint32(r) /\ is_sint32(x) /\ is_sint32(x_1) /\ is_sint32(x_2) /\ Type: is_sint32(r) /\ is_sint32(x) /\ is_sint32(x_1) /\ is_sint32(x_2) /\
is_sint32(x_3) /\ is_sint32(x_4). is_sint32(x_3) /\ is_sint32(x_4).
(* Pre-condition *) (* Pre-condition 'KO' *)
Have: P_OBS(x, x_1, r). Have: P_OBS(x, x_1, r).
} }
Prove: P_OBS(x_2, x_3, x_4). Prove: P_OBS(x_2, x_3, x_4).
......
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