[wp] fixed post labels

src/plugins/wp/tests/wp_hoare/oracle/dispatch_var2.0.res.oracle

@@ -13,20 +13,15 @@ Assume {
   (* Heap *)
   Type: is_sint32(x_1).
   (* Block In *)
-  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)).
+  Have: (Init_tmp_0=false) /\ (ta_tmp_0=false).
   (* 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_1=true) -> (Init_tmp_2=true)).
+  Have: ((Init_tmp_0=true) -> (Init_tmp_1=true)).
   (* Return *)
   Have: tmp_0 = call_global_0.
-  (* Block Out *)
-  Have: (ta_tmp_3=true).
 }
 Prove: call_global_0 = 0.
 
@@ -51,13 +46,12 @@ 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_1=true) -> (Init_tmp_2=true)).
+  Have: ((Init_tmp_0=true) -> (Init_tmp_1=true)).
 }
 Prove: (ta_tmp_0=false).
 
@@ -83,26 +77,19 @@ 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=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)).
+  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).
   (* Call 'reset' *)
-  Have: (ta_z_0=true) /\ (z = 0).
+  Have: 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: (ta_z_2=true) /\ (tmp_0 = load_0) /\ (z = load_0).
+  Have: (tmp_0 = load_0) /\ (z = load_0).
   (* Return Effects *)
-  Have: ((Init_tmp_1=true) -> (Init_tmp_2=true)).
+  Have: ((Init_tmp_0=true) -> (Init_tmp_1=true)).
   (* Return *)
   Have: tmp_0 = call_local_0.
-  (* Block Out *)
-  Have: (ta_tmp_3=true) /\ (ta_z_3=true).
 }
 Prove: call_local_0 = 0.
 
@@ -119,20 +106,17 @@ 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_2=true) /\
-      (ta_z_1=false).
+  Have: (Init_z_0=false) /\ (ta_tmp_0=false) /\ (ta_z_1=false).
   (* Merge *)
   Either {
     Case:
       Have: (Init_z_0=true) <-> (Init_z_1=true).
       (* Call 'reset' *)
-      Have: (ta_z_2=true) /\ (z = 0).
+      Have: 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)).
   }
@@ -152,11 +136,10 @@ 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_2=true) /\
-      (ta_z_1=false).
+  Have: (Init_z_0=false) /\ (ta_tmp_0=false) /\ (ta_z_1=false).
   Have: (Init_z_0=true) <-> (Init_z_1=true).
   (* Call 'reset' *)
-  Have: (ta_z_2=true) /\ (z = 0).
+  Have: z = 0.
   (* Call Effects *)
   Have: ((Init_z_1=true) -> (Init_z_2=true)).
 }
@@ -171,18 +154,16 @@ 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=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)).
+      (ta_z_0=false).
+  Have: (Init_z_0=true) <-> (Init_z_1=true).
   (* Call 'reset' *)
-  Have: (ta_z_0=true) /\ (z = 0).
+  Have: z = 0.
   (* Call Effects *)
   Have: ((Init_z_1=true) -> (Init_z_2=true)).
   (* Call 'load' *)
-  Have: (ta_z_2=true) /\ (z = load_0).
+  Have: z = load_0.
   (* Return Effects *)
-  Have: ((Init_tmp_1=true) -> (Init_tmp_2=true)).
+  Have: ((Init_tmp_0=true) -> (Init_tmp_1=true)).
 }
 Prove: (ta_tmp_0=false).
 
@@ -203,12 +184,11 @@ 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_1=true) /\
-      (ta_z_2=false).
-  Have: ((Init_z_0=true) <-> (Init_z_1=true)) /\
-      ((ta_z_1=true) <-> (ta_z_0=true)).
+  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).
   (* Call 'reset' *)
-  Have: (ta_z_1=true) /\ (z = 0).
+  Have: (ta_z_0=true) /\ (z = 0).
   (* Call Effects *)
   Have: ((Init_z_1=true) -> (Init_z_2=true)).
 }
@@ -228,22 +208,21 @@ Assume {
   (* Pre-condition *)
   Have: (ta_y_0=true).
   (* Frame In *)
-  Have: (ta_y_0=false).
+  Have: (ta_y_1=true) /\ (ta_y_0=false).
   (* Block In *)
-  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)).
+  Have: (Init_tmp_0=false) /\ (ta_tmp_0=false).
+  Have: (ta_y_1=true) <-> (ta_y_2=true).
   (* Call 'reset' *)
-  Have: y = 0.
-  Have: (ta_tmp_2=true) <-> (ta_tmp_3=true).
+  Have: (ta_y_1=true) /\ (y = 0).
+  Have: (ta_y_2=true) <-> (ta_y_3=true).
   (* Call 'load' *)
-  Have: (tmp_0 = load_0) /\ (y = load_0).
+  Have: (ta_y_2=true) /\ (tmp_0 = load_0) /\ (y = load_0).
   (* Return Effects *)
-  Have: ((Init_tmp_1=true) -> (Init_tmp_2=true)).
+  Have: ((Init_tmp_0=true) -> (Init_tmp_1=true)).
   (* Return *)
   Have: tmp_0 = call_param_0.
-  (* Block Out *)
-  Have: (ta_tmp_3=true).
+  (* Frame Out *)
+  Have: (ta_y_3=true).
 }
 Prove: call_param_0 = 0.
 
@@ -264,11 +243,14 @@ Assume {
   (* Pre-condition *)
   Have: (ta_y_1=true).
   (* Frame In *)
-  Have: (ta_y_1=false).
+  Have: (ta_y_2=true) /\ (ta_y_1=false).
   (* Block In *)
   Have: (ta_tmp_0=false).
   (* Merge *)
-  Either { Case: (* Call 'reset' *) Have: y = 0. Case: }
+  Either {
+    Case: (* Call 'reset' *) Have: (ta_y_2=true) /\ (y = 0).
+    Case: (* Exit 'reset' *) Have: (ta_y_2=true).
+  }
 }
 Prove: (ta_y_0=false).
 
@@ -289,11 +271,11 @@ Assume {
   (* Pre-condition *)
   Have: (ta_y_1=true).
   (* Frame In *)
-  Have: (ta_y_1=false).
+  Have: (ta_y_2=true) /\ (ta_y_1=false).
   (* Block In *)
   Have: (ta_tmp_0=false).
   (* Call 'reset' *)
-  Have: y = 0.
+  Have: (ta_y_2=true) /\ (y = 0).
 }
 Prove: (ta_y_0=false).
 
@@ -309,16 +291,16 @@ Assume {
   (* Pre-condition *)
   Have: (ta_y_0=true).
   (* Frame In *)
-  Have: (ta_y_0=false).
+  Have: (ta_y_1=true) /\ (ta_y_0=false).
   (* Block In *)
   Have: (Init_tmp_0=false) /\ (ta_tmp_1=false).
-  Have: (Init_tmp_0=true) <-> (Init_tmp_1=true).
+  Have: (ta_y_1=true) <-> (ta_y_2=true).
   (* Call 'reset' *)
-  Have: y = 0.
+  Have: (ta_y_1=true) /\ (y = 0).
   (* Call 'load' *)
-  Have: y = load_0.
+  Have: (ta_y_2=true) /\ (y = load_0).
   (* Return Effects *)
-  Have: ((Init_tmp_1=true) -> (Init_tmp_2=true)).
+  Have: ((Init_tmp_0=true) -> (Init_tmp_1=true)).
 }
 Prove: (ta_tmp_0=false).
 
@@ -349,11 +331,12 @@ Assume {
   (* Pre-condition *)
   Have: (ta_y_1=true).
   (* Frame In *)
-  Have: (ta_y_0=true) /\ (ta_y_1=false).
+  Have: (ta_y_2=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_0=true) /\ (y = 0).
+  Have: (ta_y_2=true) /\ (y = 0).
 }
 Prove: (ta_y_0=true).
 
@@ -367,20 +350,15 @@ 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=true) /\ (ta_tmp_1=false).
-  Have: ((Init_tmp_0=true) <-> (Init_tmp_1=true)) /\
-      ((ta_tmp_0=true) <-> (ta_tmp_2=true)).
+  Have: (Init_tmp_0=false) /\ (ta_tmp_0=false).
   (* 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_1=true) -> (Init_tmp_2=true)).
+  Have: ((Init_tmp_0=true) -> (Init_tmp_1=true)).
   (* Return *)
   Have: tmp_0 = call_param_ref_0.
-  (* Block Out *)
-  Have: (ta_tmp_3=true).
 }
 Prove: call_param_ref_0 = 0.
 
@@ -403,13 +381,12 @@ 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_1=true) -> (Init_tmp_2=true)).
+  Have: ((Init_tmp_0=true) -> (Init_tmp_1=true)).
 }
 Prove: (ta_tmp_0=false).