Update test oracles

Author: AllanBlanchard

code/acsl-logic-definitions/inductive/oracle/even-bad-2.0.res.oracle

@@ -0,0 +1 @@
+[kernel] Parsing even-bad-2.c (with preprocessing)

code/acsl-logic-definitions/inductive/oracle/even-bad-3.0.res.oracle

@@ -0,0 +1 @@
+[kernel] Parsing even-bad-3.c (with preprocessing)

code/acsl-logic-definitions/inductive/oracle/other-bad.0.res.oracle

@@ -0,0 +1,17 @@
+# frama-c -wp -wp-rte [...]
+[kernel] Parsing other-bad.c (with preprocessing)
+[wp] Running WP plugin...
+[rte:annot] annotating function foo
+[wp] [Valid] Goal foo_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal foo_terminates (Cfg) (Trivial)
+[wp] 1 goal scheduled
+[wp] User Error: After simplification inductive P appear ill-formed (hint: check cases premises)
+[wp] Warning: Goal Property: running prover Alt-Ergo:2.6.1 failed ([User Error])
+[wp] [Failure] typed_foo_ensures (Alt-Ergo) (No Cache)
+[wp] Proved goals:    2 / 3
+  Terminating:     1
+  Unreachable:     1
+  Failed:          1
+[wp:pedantic-assigns] other-bad.c:8: Warning: 
+  No 'assigns' specification for function 'foo'.
+  Callers assumptions might be imprecise.

code/function-contract/contract/oracle/abs-4.0.res.oracle

@@ -5,8 +5,8 @@
 [wp] [Valid] Goal abs_exits (Cfg) (Unreachable)
 [wp] [Valid] Goal abs_terminates (Cfg) (Trivial)
 [wp] 3 goals scheduled
+[wp] [Valid] typed_abs_ensures_positive_value_function_result (Qed)
 [wp] [Valid] typed_abs_ensures (Qed)
-[wp] [Valid] typed_abs_ensures_2 (Qed)
 [wp] [Valid] typed_abs_assert_rte_signed_overflow (Qed)
 [wp] Proved goals:    5 / 5
   Terminating:     1

code/function-contract/contract/oracle/abs-5.0.res.oracle

@@ -6,8 +6,8 @@
 [wp] [Valid] Goal abs_exits (Cfg) (Unreachable)
 [wp] [Valid] Goal abs_terminates (Cfg) (Trivial)
 [wp] 9 goals scheduled
+[wp] [Valid] typed_abs_ensures_positive_value_function_result (Qed)
 [wp] [Valid] typed_abs_ensures (Qed)
-[wp] [Valid] typed_abs_ensures_2 (Qed)
 [wp] [Valid] typed_abs_assert_rte_signed_overflow (Qed)
 [wp] [Valid] typed_foo_terminates (Qed)
 [wp] [Valid] typed_foo_exits (Qed)

code/statements/loops/oracle/check-admit-invariant.0.res.oracle

@@ -33,23 +33,27 @@ Prover Qed returns Valid
 Goal Preservation of Invariant 'C3' (file check-admit-invariant.c, line 10):
 Assume {
   Type: is_sint32(x) /\ is_sint32(x_1) /\ is_sint32(x_2) /\ is_sint32(y) /\
-      is_sint32(y_1).
+      is_sint32(y_1) /\ is_sint32(y_2).
   (* Initializer *)
   Init: (Init_x_0=true).
   (* Initializer *)
   Init: x_2 = 0.
   (* Initializer *)
-  Init: y_1 = 0.
+  Init: (Init_y_0=true).
+  (* Initializer *)
+  Init: y_2 = 0.
   (* Invariant 'I1' *)
   Have: 0 <= x_2.
   (* Invariant 'A2' *)
   Have: x_2 <= 10.
   (* Invariant 'C3' *)
-  Have: y_1 <= 20.
+  Have: y_2 <= 20.
   (* Invariant 'I4' *)
-  Have: (2 * x_2) = y_1.
+  Have: (2 * x_2) = y_2.
   (* Loop assigns ... *)
-  Have: ((Init_x_0=true) -> (Init_x_1=true)).
+  Have: ((Init_x_1=true) <-> (Init_x_0=true)) /\
+      (((Init_x_1=true) -> (Init_x_2=true))) /\
+      (((Init_y_0=true) -> (Init_y_1=true))).
   (* Invariant 'I1' *)
   Have: 0 <= x_1.
   (* Invariant 'A2' *)
@@ -92,21 +96,25 @@ Prover Qed returns Valid
 Goal Preservation of Invariant 'I4' (file check-admit-invariant.c, line 11):
 Assume {
   Type: is_sint32(x) /\ is_sint32(x_1) /\ is_sint32(x_2) /\ is_sint32(y) /\
-      is_sint32(y_1).
+      is_sint32(y_1) /\ is_sint32(y_2).
   (* Initializer *)
   Init: (Init_x_0=true).
   (* Initializer *)
   Init: x_2 = 0.
   (* Initializer *)
-  Init: y_1 = 0.
+  Init: (Init_y_0=true).
+  (* Initializer *)
+  Init: y_2 = 0.
   (* Invariant 'I1' *)
   Have: 0 <= x_2.
   (* Invariant 'A2' *)
   Have: x_2 <= 10.
   (* Invariant 'I4' *)
-  Have: (2 * x_2) = y_1.
+  Have: (2 * x_2) = y_2.
   (* Loop assigns ... *)
-  Have: ((Init_x_0=true) -> (Init_x_1=true)).
+  Have: ((Init_x_1=true) <-> (Init_x_0=true)) /\
+      (((Init_x_1=true) -> (Init_x_2=true))) /\
+      (((Init_y_0=true) -> (Init_y_1=true))).
   (* Invariant 'I1' *)
   Have: 0 <= x_1.
   (* Invariant 'A2' *)

code/statements/loops/oracle/unreachable.0.res.oracle

@@ -0,0 +1,14 @@
+# frama-c -wp -wp-rte [...]
+[kernel] Parsing unreachable.c (with preprocessing)
+[wp] Running WP plugin...
+[rte:annot] annotating function bar
+[wp] [Valid] Goal bar_assert (Cfg) (Unreachable)
+[wp] [Valid] Goal bar_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal bar_terminates (Cfg) (Trivial)
+[wp] Warning: No goal generated
+[wp] Proved goals:    3 / 3
+  Terminating:     1
+  Unreachable:     2
+[wp:pedantic-assigns] unreachable.c:1: Warning: 
+  No 'assigns' specification for function 'bar'.
+  Callers assumptions might be imprecise.