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

[wp] named pre-conditions 

with also variable renaming
parent 61ce82b2
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/flash.0.res.oracle
+ 42
− 27
View file @ def3f91d
...@@ -27,16 +27,19 @@ Let x_3 = OBSERVER_time_0 - 1. ...@@ -27,16 +27,19 @@ Let x_3 = OBSERVER_time_0 - 1.
Let x_4 = RD_time_0 - 1. Let x_4 = RD_time_0 - 1.
Let a_8 = L_RD_current(x_4). Let a_8 = L_RD_current(x_4).
Let x_5 = OBSERVER_time_0 - 2. Let x_5 = OBSERVER_time_0 - 2.
Let x_6 = OBSERVER_time_0 - 3. Let x_6 = RD_time_0 - 2.
Let x_7 = RD_time_0 - 2. Let x_7 = OBSERVER_time_0 - 3.
Assume { Assume {
Type: is_sint32(OBSERVER_time_0) /\ is_sint32(RD_time_0) /\ Type: is_sint32(OBSERVER_time_0) /\ is_sint32(RD_time_0) /\
is_sint32(WR_time_0) /\ is_sint32(x_6) /\ is_sint32(x_5) /\ is_sint32(WR_time_0) /\ is_sint32(x_7) /\ is_sint32(x_5) /\
is_sint32(x_7) /\ is_sint32(x_3) /\ is_sint32(x_4) /\ is_sint32(x) /\ is_sint32(x_6) /\ is_sint32(x_3) /\ is_sint32(x_4) /\ is_sint32(x) /\
is_sint32(x_1) /\ is_sint32(x_2). is_sint32(x_1) /\ is_sint32(x_2).
(* Pre-condition *) (* Pre-condition *)
Have: (L_WR_current(WR_time_0) = L_INDEX_init) /\ Have: L_OBSERVER(x_7) = nil.
(L_OBSERVER(x_6) = nil) /\ (L_RD_current(x_7) = L_INDEX_init). (* Pre-condition *)
Have: L_RD_current(x_6) = L_INDEX_init.
(* Pre-condition *)
Have: L_WR_current(WR_time_0) = L_INDEX_init.
(* Call 'RD' *) (* Call 'RD' *)
Have: (a_5 = a_8) /\ (L_OBSERVER(x_5) = [ a_1 ]) /\ Have: (a_5 = a_8) /\ (L_OBSERVER(x_5) = [ a_1 ]) /\
((L_RD_value(a, L_RD_access(L_INDEX_init, a)) ((L_RD_value(a, L_RD_access(L_INDEX_init, a))
...@@ -71,16 +74,19 @@ Let x_3 = OBSERVER_time_0 - 1. ...@@ -71,16 +74,19 @@ Let x_3 = OBSERVER_time_0 - 1.
Let x_4 = RD_time_0 - 1. Let x_4 = RD_time_0 - 1.
Let a_8 = L_RD_current(x_4). Let a_8 = L_RD_current(x_4).
Let x_5 = OBSERVER_time_0 - 2. Let x_5 = OBSERVER_time_0 - 2.
Let x_6 = OBSERVER_time_0 - 3. Let x_6 = RD_time_0 - 2.
Let x_7 = RD_time_0 - 2. Let x_7 = OBSERVER_time_0 - 3.
Assume { Assume {
Type: is_sint32(OBSERVER_time_0) /\ is_sint32(RD_time_0) /\ Type: is_sint32(OBSERVER_time_0) /\ is_sint32(RD_time_0) /\
is_sint32(WR_time_0) /\ is_sint32(x_6) /\ is_sint32(x_5) /\ is_sint32(WR_time_0) /\ is_sint32(x_7) /\ is_sint32(x_5) /\
is_sint32(x_7) /\ is_sint32(x_3) /\ is_sint32(x_4) /\ is_sint32(x) /\ is_sint32(x_6) /\ is_sint32(x_3) /\ is_sint32(x_4) /\ is_sint32(x) /\
is_sint32(x_1) /\ is_sint32(x_2). is_sint32(x_1) /\ is_sint32(x_2).
(* Pre-condition *) (* Pre-condition *)
Have: (L_WR_current(WR_time_0) = L_INDEX_init) /\ Have: L_OBSERVER(x_7) = nil.
(L_OBSERVER(x_6) = nil) /\ (L_RD_current(x_7) = L_INDEX_init). (* Pre-condition *)
Have: L_RD_current(x_6) = L_INDEX_init.
(* Pre-condition *)
Have: L_WR_current(WR_time_0) = L_INDEX_init.
(* Call 'RD' *) (* Call 'RD' *)
Have: (a_5 = a_8) /\ (L_OBSERVER(x_5) = [ a_1 ]) /\ Have: (a_5 = a_8) /\ (L_OBSERVER(x_5) = [ a_1 ]) /\
((L_RD_value(a, L_RD_access(L_INDEX_init, a)) ((L_RD_value(a, L_RD_access(L_INDEX_init, a))
...@@ -115,16 +121,19 @@ Let x_3 = OBSERVER_time_0 - 1. ...@@ -115,16 +121,19 @@ Let x_3 = OBSERVER_time_0 - 1.
Let x_4 = RD_time_0 - 2. Let x_4 = RD_time_0 - 2.
Let a_8 = L_RD_current(x_4). Let a_8 = L_RD_current(x_4).
Let x_5 = OBSERVER_time_0 - 2. Let x_5 = OBSERVER_time_0 - 2.
Let x_6 = OBSERVER_time_0 - 3. Let x_6 = RD_time_0 - 3.
Let x_7 = RD_time_0 - 3. Let x_7 = OBSERVER_time_0 - 3.
Assume { Assume {
Type: is_sint32(OBSERVER_time_0) /\ is_sint32(RD_time_0) /\ Type: is_sint32(OBSERVER_time_0) /\ is_sint32(RD_time_0) /\
is_sint32(WR_time_0) /\ is_sint32(x_6) /\ is_sint32(x_7) /\ is_sint32(WR_time_0) /\ is_sint32(x_7) /\ is_sint32(x_6) /\
is_sint32(x_5) /\ is_sint32(x_4) /\ is_sint32(x_3) /\ is_sint32(x_2) /\ is_sint32(x_5) /\ is_sint32(x_4) /\ is_sint32(x_3) /\ is_sint32(x_2) /\
is_sint32(x) /\ is_sint32(x_1). is_sint32(x) /\ is_sint32(x_1).
(* Pre-condition *) (* Pre-condition *)
Have: (L_WR_current(WR_time_0) = L_INDEX_init) /\ Have: L_OBSERVER(x_7) = nil.
(L_OBSERVER(x_6) = nil) /\ (L_RD_current(x_7) = L_INDEX_init). (* Pre-condition *)
Have: L_RD_current(x_6) = L_INDEX_init.
(* Pre-condition *)
Have: L_WR_current(WR_time_0) = L_INDEX_init.
(* Call 'RD' *) (* Call 'RD' *)
Have: (a_5 = a_8) /\ (L_OBSERVER(x_5) = [ a_1 ]) /\ Have: (a_5 = a_8) /\ (L_OBSERVER(x_5) = [ a_1 ]) /\
((L_RD_value(a, L_RD_access(L_INDEX_init, a)) ((L_RD_value(a, L_RD_access(L_INDEX_init, a))
...@@ -159,16 +168,19 @@ Let x_4 = RD_time_0 - 2. ...@@ -159,16 +168,19 @@ Let x_4 = RD_time_0 - 2.
Let a_7 = L_RD_current(x_4). Let a_7 = L_RD_current(x_4).
Let x_5 = OBSERVER_time_0 - 2. Let x_5 = OBSERVER_time_0 - 2.
Let x_6 = L_RD_value(a, L_RD_access(L_INDEX_init, a)). Let x_6 = L_RD_value(a, L_RD_access(L_INDEX_init, a)).
Let x_7 = OBSERVER_time_0 - 3. Let x_7 = RD_time_0 - 3.
Let x_8 = RD_time_0 - 3. Let x_8 = OBSERVER_time_0 - 3.
Assume { Assume {
Type: is_sint32(OBSERVER_time_0) /\ is_sint32(RD_time_0) /\ Type: is_sint32(OBSERVER_time_0) /\ is_sint32(RD_time_0) /\
is_sint32(WR_time_0) /\ is_sint32(x_7) /\ is_sint32(x_8) /\ is_sint32(WR_time_0) /\ is_sint32(x_8) /\ is_sint32(x_7) /\
is_sint32(x_5) /\ is_sint32(x_4) /\ is_sint32(x_3) /\ is_sint32(x_2) /\ is_sint32(x_5) /\ is_sint32(x_4) /\ is_sint32(x_3) /\ is_sint32(x_2) /\
is_sint32(x) /\ is_sint32(x_1). is_sint32(x) /\ is_sint32(x_1).
(* Pre-condition *) (* Pre-condition *)
Have: (L_WR_current(WR_time_0) = L_INDEX_init) /\ Have: L_OBSERVER(x_8) = nil.
(L_OBSERVER(x_7) = nil) /\ (L_RD_current(x_8) = L_INDEX_init). (* Pre-condition *)
Have: L_RD_current(x_7) = L_INDEX_init.
(* Pre-condition *)
Have: L_WR_current(WR_time_0) = L_INDEX_init.
(* Call 'RD' *) (* Call 'RD' *)
Have: (a_5 = a_7) /\ (L_OBSERVER(x_5) = [ a_1 ]) /\ Have: (a_5 = a_7) /\ (L_OBSERVER(x_5) = [ a_1 ]) /\
((x_6 + L_RD_value(a_2, L_RD_access(a_7, a_2))) ((x_6 + L_RD_value(a_2, L_RD_access(a_7, a_2)))
...@@ -203,16 +215,19 @@ Let x_3 = OBSERVER_time_0 - 1. ...@@ -203,16 +215,19 @@ Let x_3 = OBSERVER_time_0 - 1.
Let x_4 = RD_time_0 - 2. Let x_4 = RD_time_0 - 2.
Let a_7 = L_RD_current(x_4). Let a_7 = L_RD_current(x_4).
Let x_5 = OBSERVER_time_0 - 2. Let x_5 = OBSERVER_time_0 - 2.
Let x_6 = OBSERVER_time_0 - 3. Let x_6 = RD_time_0 - 3.
Let x_7 = RD_time_0 - 3. Let x_7 = OBSERVER_time_0 - 3.
Assume { Assume {
Type: is_sint32(OBSERVER_time_0) /\ is_sint32(RD_time_0) /\ Type: is_sint32(OBSERVER_time_0) /\ is_sint32(RD_time_0) /\
is_sint32(WR_time_0) /\ is_sint32(x_6) /\ is_sint32(x_7) /\ is_sint32(WR_time_0) /\ is_sint32(x_7) /\ is_sint32(x_6) /\
is_sint32(x_5) /\ is_sint32(x_4) /\ is_sint32(x_3) /\ is_sint32(x_2) /\ is_sint32(x_5) /\ is_sint32(x_4) /\ is_sint32(x_3) /\ is_sint32(x_2) /\
is_sint32(x) /\ is_sint32(x_1). is_sint32(x) /\ is_sint32(x_1).
(* Pre-condition *) (* Pre-condition *)
Have: (L_WR_current(WR_time_0) = L_INDEX_init) /\ Have: L_OBSERVER(x_7) = nil.
(L_OBSERVER(x_6) = nil) /\ (L_RD_current(x_7) = L_INDEX_init). (* Pre-condition *)
Have: L_RD_current(x_6) = L_INDEX_init.
(* Pre-condition *)
Have: L_WR_current(WR_time_0) = L_INDEX_init.
(* Call 'RD' *) (* Call 'RD' *)
Have: (a_5 = a_7) /\ (L_OBSERVER(x_5) = [ a_1 ]) /\ Have: (a_5 = a_7) /\ (L_OBSERVER(x_5) = [ a_1 ]) /\
((L_RD_value(a, L_RD_access(L_INDEX_init, a)) ((L_RD_value(a, L_RD_access(L_INDEX_init, a))
......
src/plugins/wp/tests/wp_plugin/oracle/flash.1.res.oracle
+ 42
− 27
View file @ def3f91d
...@@ -29,16 +29,19 @@ Let x_3 = OBSERVER_time_0 - 1. ...@@ -29,16 +29,19 @@ Let x_3 = OBSERVER_time_0 - 1.
Let x_4 = RD_time_0 - 1. Let x_4 = RD_time_0 - 1.
Let a_8 = L_RD_current(x_4). Let a_8 = L_RD_current(x_4).
Let x_5 = OBSERVER_time_0 - 2. Let x_5 = OBSERVER_time_0 - 2.
Let x_6 = OBSERVER_time_0 - 3. Let x_6 = RD_time_0 - 2.
Let x_7 = RD_time_0 - 2. Let x_7 = OBSERVER_time_0 - 3.
Assume { Assume {
Type: is_sint32(OBSERVER_time_0) /\ is_sint32(RD_time_0) /\ Type: is_sint32(OBSERVER_time_0) /\ is_sint32(RD_time_0) /\
is_sint32(WR_time_0) /\ is_sint32(x_6) /\ is_sint32(x_5) /\ is_sint32(WR_time_0) /\ is_sint32(x_7) /\ is_sint32(x_5) /\
is_sint32(x_7) /\ is_sint32(x_3) /\ is_sint32(x_4) /\ is_sint32(x) /\ is_sint32(x_6) /\ is_sint32(x_3) /\ is_sint32(x_4) /\ is_sint32(x) /\
is_sint32(x_1) /\ is_sint32(x_2). is_sint32(x_1) /\ is_sint32(x_2).
(* Pre-condition *) (* Pre-condition *)
Have: (L_WR_current(WR_time_0) = const(0)) /\ (L_OBSERVER(x_6) = nil) /\ Have: L_OBSERVER(x_7) = nil.
(L_RD_current(x_7) = const(0)). (* Pre-condition *)
Have: L_RD_current(x_6) = const(0).
(* Pre-condition *)
Have: L_WR_current(WR_time_0) = const(0).
(* Call 'RD' *) (* Call 'RD' *)
Have: (a_8 = a_5) /\ (L_OBSERVER(x_5) = [ a_1 ]) /\ Have: (a_8 = a_5) /\ (L_OBSERVER(x_5) = [ a_1 ]) /\
((L_RD_value(a, (const(0))[a]) + L_RD_value(a_2, (a_8)[a_2])) ((L_RD_value(a, (const(0))[a]) + L_RD_value(a_2, (a_8)[a_2]))
...@@ -72,16 +75,19 @@ Let x_3 = OBSERVER_time_0 - 1. ...@@ -72,16 +75,19 @@ Let x_3 = OBSERVER_time_0 - 1.
Let x_4 = RD_time_0 - 1. Let x_4 = RD_time_0 - 1.
Let a_8 = L_RD_current(x_4). Let a_8 = L_RD_current(x_4).
Let x_5 = OBSERVER_time_0 - 2. Let x_5 = OBSERVER_time_0 - 2.
Let x_6 = OBSERVER_time_0 - 3. Let x_6 = RD_time_0 - 2.
Let x_7 = RD_time_0 - 2. Let x_7 = OBSERVER_time_0 - 3.
Assume { Assume {
Type: is_sint32(OBSERVER_time_0) /\ is_sint32(RD_time_0) /\ Type: is_sint32(OBSERVER_time_0) /\ is_sint32(RD_time_0) /\
is_sint32(WR_time_0) /\ is_sint32(x_6) /\ is_sint32(x_5) /\ is_sint32(WR_time_0) /\ is_sint32(x_7) /\ is_sint32(x_5) /\
is_sint32(x_7) /\ is_sint32(x_3) /\ is_sint32(x_4) /\ is_sint32(x) /\ is_sint32(x_6) /\ is_sint32(x_3) /\ is_sint32(x_4) /\ is_sint32(x) /\
is_sint32(x_1) /\ is_sint32(x_2). is_sint32(x_1) /\ is_sint32(x_2).
(* Pre-condition *) (* Pre-condition *)
Have: (L_WR_current(WR_time_0) = const(0)) /\ (L_OBSERVER(x_6) = nil) /\ Have: L_OBSERVER(x_7) = nil.
(L_RD_current(x_7) = const(0)). (* Pre-condition *)
Have: L_RD_current(x_6) = const(0).
(* Pre-condition *)
Have: L_WR_current(WR_time_0) = const(0).
(* Call 'RD' *) (* Call 'RD' *)
Have: (a_8 = a_5) /\ (L_OBSERVER(x_5) = [ a_1 ]) /\ Have: (a_8 = a_5) /\ (L_OBSERVER(x_5) = [ a_1 ]) /\
((L_RD_value(a, (const(0))[a]) + L_RD_value(a_2, (a_8)[a_2])) ((L_RD_value(a, (const(0))[a]) + L_RD_value(a_2, (a_8)[a_2]))
...@@ -115,16 +121,19 @@ Let x_3 = OBSERVER_time_0 - 1. ...@@ -115,16 +121,19 @@ Let x_3 = OBSERVER_time_0 - 1.
Let x_4 = RD_time_0 - 2. Let x_4 = RD_time_0 - 2.
Let a_8 = L_RD_current(x_4). Let a_8 = L_RD_current(x_4).
Let x_5 = OBSERVER_time_0 - 2. Let x_5 = OBSERVER_time_0 - 2.
Let x_6 = OBSERVER_time_0 - 3. Let x_6 = RD_time_0 - 3.
Let x_7 = RD_time_0 - 3. Let x_7 = OBSERVER_time_0 - 3.
Assume { Assume {
Type: is_sint32(OBSERVER_time_0) /\ is_sint32(RD_time_0) /\ Type: is_sint32(OBSERVER_time_0) /\ is_sint32(RD_time_0) /\
is_sint32(WR_time_0) /\ is_sint32(x_6) /\ is_sint32(x_7) /\ is_sint32(WR_time_0) /\ is_sint32(x_7) /\ is_sint32(x_6) /\
is_sint32(x_5) /\ is_sint32(x_4) /\ is_sint32(x_3) /\ is_sint32(x_2) /\ is_sint32(x_5) /\ is_sint32(x_4) /\ is_sint32(x_3) /\ is_sint32(x_2) /\
is_sint32(x) /\ is_sint32(x_1). is_sint32(x) /\ is_sint32(x_1).
(* Pre-condition *) (* Pre-condition *)
Have: (L_WR_current(WR_time_0) = const(0)) /\ (L_OBSERVER(x_6) = nil) /\ Have: L_OBSERVER(x_7) = nil.
(L_RD_current(x_7) = const(0)). (* Pre-condition *)
Have: L_RD_current(x_6) = const(0).
(* Pre-condition *)
Have: L_WR_current(WR_time_0) = const(0).
(* Call 'RD' *) (* Call 'RD' *)
Have: (a_8 = a_5) /\ (L_OBSERVER(x_5) = [ a_1 ]) /\ Have: (a_8 = a_5) /\ (L_OBSERVER(x_5) = [ a_1 ]) /\
((L_RD_value(a, (const(0))[a]) + L_RD_value(a_2, (a_8)[a_2])) ((L_RD_value(a, (const(0))[a]) + L_RD_value(a_2, (a_8)[a_2]))
...@@ -158,16 +167,19 @@ Let x_4 = RD_time_0 - 2. ...@@ -158,16 +167,19 @@ Let x_4 = RD_time_0 - 2.
Let a_7 = L_RD_current(x_4). Let a_7 = L_RD_current(x_4).
Let x_5 = OBSERVER_time_0 - 2. Let x_5 = OBSERVER_time_0 - 2.
Let x_6 = L_RD_value(a, (const(0))[a]). Let x_6 = L_RD_value(a, (const(0))[a]).
Let x_7 = OBSERVER_time_0 - 3. Let x_7 = RD_time_0 - 3.
Let x_8 = RD_time_0 - 3. Let x_8 = OBSERVER_time_0 - 3.
Assume { Assume {
Type: is_sint32(OBSERVER_time_0) /\ is_sint32(RD_time_0) /\ Type: is_sint32(OBSERVER_time_0) /\ is_sint32(RD_time_0) /\
is_sint32(WR_time_0) /\ is_sint32(x_7) /\ is_sint32(x_8) /\ is_sint32(WR_time_0) /\ is_sint32(x_8) /\ is_sint32(x_7) /\
is_sint32(x_5) /\ is_sint32(x_4) /\ is_sint32(x_3) /\ is_sint32(x_2) /\ is_sint32(x_5) /\ is_sint32(x_4) /\ is_sint32(x_3) /\ is_sint32(x_2) /\
is_sint32(x) /\ is_sint32(x_1). is_sint32(x) /\ is_sint32(x_1).
(* Pre-condition *) (* Pre-condition *)
Have: (L_WR_current(WR_time_0) = const(0)) /\ (L_OBSERVER(x_7) = nil) /\ Have: L_OBSERVER(x_8) = nil.
(L_RD_current(x_8) = const(0)). (* Pre-condition *)
Have: L_RD_current(x_7) = const(0).
(* Pre-condition *)
Have: L_WR_current(WR_time_0) = const(0).
(* Call 'RD' *) (* Call 'RD' *)
Have: (a_7 = a_5) /\ (L_OBSERVER(x_5) = [ a_1 ]) /\ Have: (a_7 = a_5) /\ (L_OBSERVER(x_5) = [ a_1 ]) /\
((x_6 + L_RD_value(a_2, (a_7)[a_2])) = L_WR_value(a_2, (const(0))[a_2])). ((x_6 + L_RD_value(a_2, (a_7)[a_2])) = L_WR_value(a_2, (const(0))[a_2])).
...@@ -200,16 +212,19 @@ Let x_3 = OBSERVER_time_0 - 1. ...@@ -200,16 +212,19 @@ Let x_3 = OBSERVER_time_0 - 1.
Let x_4 = RD_time_0 - 2. Let x_4 = RD_time_0 - 2.
Let a_7 = L_RD_current(x_4). Let a_7 = L_RD_current(x_4).
Let x_5 = OBSERVER_time_0 - 2. Let x_5 = OBSERVER_time_0 - 2.
Let x_6 = OBSERVER_time_0 - 3. Let x_6 = RD_time_0 - 3.
Let x_7 = RD_time_0 - 3. Let x_7 = OBSERVER_time_0 - 3.
Assume { Assume {
Type: is_sint32(OBSERVER_time_0) /\ is_sint32(RD_time_0) /\ Type: is_sint32(OBSERVER_time_0) /\ is_sint32(RD_time_0) /\
is_sint32(WR_time_0) /\ is_sint32(x_6) /\ is_sint32(x_7) /\ is_sint32(WR_time_0) /\ is_sint32(x_7) /\ is_sint32(x_6) /\
is_sint32(x_5) /\ is_sint32(x_4) /\ is_sint32(x_3) /\ is_sint32(x_2) /\ is_sint32(x_5) /\ is_sint32(x_4) /\ is_sint32(x_3) /\ is_sint32(x_2) /\
is_sint32(x) /\ is_sint32(x_1). is_sint32(x) /\ is_sint32(x_1).
(* Pre-condition *) (* Pre-condition *)
Have: (L_WR_current(WR_time_0) = const(0)) /\ (L_OBSERVER(x_6) = nil) /\ Have: L_OBSERVER(x_7) = nil.
(L_RD_current(x_7) = const(0)). (* Pre-condition *)
Have: L_RD_current(x_6) = const(0).
(* Pre-condition *)
Have: L_WR_current(WR_time_0) = const(0).
(* Call 'RD' *) (* Call 'RD' *)
Have: (a_7 = a_5) /\ (L_OBSERVER(x_5) = [ a_1 ]) /\ Have: (a_7 = a_5) /\ (L_OBSERVER(x_5) = [ a_1 ]) /\
((L_RD_value(a, (const(0))[a]) + L_RD_value(a_2, (a_7)[a_2])) ((L_RD_value(a, (const(0))[a]) + L_RD_value(a_2, (a_7)[a_2]))
......
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