From f8cfd651bbebfc9ac9c7ae45bbc762fbfa8c955f Mon Sep 17 00:00:00 2001
From: Patrick Baudin <patrick.baudin@cea.fr>
Date: Wed, 22 Dec 2021 10:21:33 +0100
Subject: [PATCH] [Tests] oracle updates
---
tests/meta-deduce/oracle/consequence.res.oracle | 2 +-
tests/meta-deduce/oracle/deduction_with_offset.res.oracle | 2 +-
tests/meta-deduce/oracle/negative_assigns.res.oracle | 2 +-
tests/meta-wp/oracle/assert_type_of.res.oracle | 2 +-
tests/meta-wp/oracle/axiomatic_requires.res.oracle | 2 +-
tests/meta-wp/oracle/dummy.res.oracle | 6 +++---
tests/meta-wp/oracle/forbidden.res.oracle | 2 +-
tests/meta-wp/oracle/invariant.res.oracle | 6 +++---
tests/meta-wp/oracle/loop_invariant.res.oracle | 2 +-
tests/meta-wp/oracle/monotony.res.oracle | 2 +-
tests/meta-wp/oracle/options.0.res.oracle | 2 +-
tests/meta-wp/oracle/options.1.res.oracle | 2 +-
tests/meta-wp/oracle/pre_label.res.oracle | 2 +-
tests/meta-wp/oracle/typing.res.oracle | 8 ++++----
tests/meta-wp/oracle/uncalled.res.oracle | 2 +-
tests/meta/oracle/absent.0.res.oracle | 2 +-
tests/meta/oracle/absent.1.res.oracle | 2 +-
tests/meta/oracle/bindings_test.res.oracle | 2 +-
tests/meta/oracle/called_arg.res.oracle | 2 +-
tests/meta/oracle/callees.res.oracle | 4 ++--
tests/meta/oracle/func_meta_var.res.oracle | 2 +-
tests/meta/oracle/named.res.oracle | 2 +-
tests/meta/oracle/number_assertions.0.res.oracle | 2 +-
tests/meta/oracle/passthrough.res.oracle | 2 +-
tests/meta/oracle/quantif.res.oracle | 2 +-
tests/meta/oracle/read_addrof.res.oracle | 2 +-
tests/meta/oracle/renaming.res.oracle | 2 +-
tests/meta/oracle/simplify.res.oracle | 2 +-
tests/meta/oracle/temp_variables.res.oracle | 2 +-
tests/meta/oracle/unspecified_sequence.res.oracle | 2 +-
30 files changed, 38 insertions(+), 38 deletions(-)
diff --git a/tests/meta-deduce/oracle/consequence.res.oracle b/tests/meta-deduce/oracle/consequence.res.oracle
index 20cb730..5ce7fbd 100644
--- a/tests/meta-deduce/oracle/consequence.res.oracle
+++ b/tests/meta-deduce/oracle/consequence.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/meta-deduce/consequence.c (with preprocessing)
+[kernel] Parsing consequence.c (with preprocessing)
[meta] Translation is enabled
[meta] Will process 7 properties
[meta] inv_small : OK
diff --git a/tests/meta-deduce/oracle/deduction_with_offset.res.oracle b/tests/meta-deduce/oracle/deduction_with_offset.res.oracle
index a5f4290..6c45864 100644
--- a/tests/meta-deduce/oracle/deduction_with_offset.res.oracle
+++ b/tests/meta-deduce/oracle/deduction_with_offset.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/meta-deduce/deduction_with_offset.c (with preprocessing)
+[kernel] Parsing deduction_with_offset.c (with preprocessing)
[meta] Translation is enabled
[meta] Will process 7 properties
[meta] d1 : OK
diff --git a/tests/meta-deduce/oracle/negative_assigns.res.oracle b/tests/meta-deduce/oracle/negative_assigns.res.oracle
index 43ea6cd..9321887 100644
--- a/tests/meta-deduce/oracle/negative_assigns.res.oracle
+++ b/tests/meta-deduce/oracle/negative_assigns.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/meta-deduce/negative_assigns.c (with preprocessing)
+[kernel] Parsing negative_assigns.c (with preprocessing)
[meta] Translation is enabled
[meta] Will process 3 properties
[meta] Warning: nega_incomplete : FAILURE
diff --git a/tests/meta-wp/oracle/assert_type_of.res.oracle b/tests/meta-wp/oracle/assert_type_of.res.oracle
index 43fdbdc..fdc43b1 100644
--- a/tests/meta-wp/oracle/assert_type_of.res.oracle
+++ b/tests/meta-wp/oracle/assert_type_of.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/meta-wp/assert_type_of.c (with preprocessing)
+[kernel] Parsing assert_type_of.c (with preprocessing)
[meta] Translation is enabled
[meta] Will process 3 properties
[meta] Successful translation
diff --git a/tests/meta-wp/oracle/axiomatic_requires.res.oracle b/tests/meta-wp/oracle/axiomatic_requires.res.oracle
index 03f1412..db2ced8 100644
--- a/tests/meta-wp/oracle/axiomatic_requires.res.oracle
+++ b/tests/meta-wp/oracle/axiomatic_requires.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/meta-wp/axiomatic_requires.c (with preprocessing)
+[kernel] Parsing axiomatic_requires.c (with preprocessing)
[meta] Translation is enabled
[meta] Will process 1 properties
[meta] Successful translation
diff --git a/tests/meta-wp/oracle/dummy.res.oracle b/tests/meta-wp/oracle/dummy.res.oracle
index ec1cf8f..358bcc5 100644
--- a/tests/meta-wp/oracle/dummy.res.oracle
+++ b/tests/meta-wp/oracle/dummy.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/meta-wp/dummy.c (with preprocessing)
+[kernel] Parsing dummy.c (with preprocessing)
[meta] Translation is enabled
[meta] Will process 6 properties
[meta] Successful translation
@@ -47,7 +47,7 @@
[wp] Proved goals: 39 / 39
Qed: 38
Alt-Ergo: 1
-[wp] tests/meta-wp/dummy.c:22: Warning:
+[wp] dummy.c:22: Warning:
Memory model hypotheses for function 'RW':
/*@
behavior wp_typed:
@@ -55,7 +55,7 @@
requires \separated(a, &ROOT_BYTE, &NOP, &checkSum);
*/
void RW(int *a, int *b);
-[wp] tests/meta-wp/dummy.c:31: Warning:
+[wp] dummy.c:31: Warning:
Memory model hypotheses for function 'compute':
/*@ behavior wp_typed:
requires \separated(a, &NOP, &checkSum, &STATE); */
diff --git a/tests/meta-wp/oracle/forbidden.res.oracle b/tests/meta-wp/oracle/forbidden.res.oracle
index 3a7e4d8..3c5e658 100644
--- a/tests/meta-wp/oracle/forbidden.res.oracle
+++ b/tests/meta-wp/oracle/forbidden.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/meta-wp/forbidden.c (with preprocessing)
+[kernel] Parsing forbidden.c (with preprocessing)
[meta] Translation is enabled
[meta] Will process 1 properties
[meta] Successful translation
diff --git a/tests/meta-wp/oracle/invariant.res.oracle b/tests/meta-wp/oracle/invariant.res.oracle
index 2cf5a2c..13970de 100644
--- a/tests/meta-wp/oracle/invariant.res.oracle
+++ b/tests/meta-wp/oracle/invariant.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/meta-wp/invariant.c (with preprocessing)
+[kernel] Parsing invariant.c (with preprocessing)
[meta] Translation is enabled
[meta] Will process 4 properties
[meta] Successful translation
@@ -45,8 +45,8 @@ unsigned int B;
*/
void requiresInv(void)
{
- __FC_assert((A % (unsigned int)2 == (unsigned int)0) != 0,
- "tests/meta-wp/invariant.c",11,"A % 2 == 0");
+ __FC_assert((A % (unsigned int)2 == (unsigned int)0) != 0,"invariant.c",11,
+ "A % 2 == 0");
return;
}
diff --git a/tests/meta-wp/oracle/loop_invariant.res.oracle b/tests/meta-wp/oracle/loop_invariant.res.oracle
index dd9cf16..320b858 100644
--- a/tests/meta-wp/oracle/loop_invariant.res.oracle
+++ b/tests/meta-wp/oracle/loop_invariant.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/meta-wp/loop_invariant.c (with preprocessing)
+[kernel] Parsing loop_invariant.c (with preprocessing)
[meta] Translation is enabled
[meta] Will process 1 properties
[meta] Successful translation
diff --git a/tests/meta-wp/oracle/monotony.res.oracle b/tests/meta-wp/oracle/monotony.res.oracle
index 9c2212d..0afaf53 100644
--- a/tests/meta-wp/oracle/monotony.res.oracle
+++ b/tests/meta-wp/oracle/monotony.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/meta-wp/monotony.c (with preprocessing)
+[kernel] Parsing monotony.c (with preprocessing)
[meta] Translation is enabled
[meta] Will process 1 properties
[meta] Successful translation
diff --git a/tests/meta-wp/oracle/options.0.res.oracle b/tests/meta-wp/oracle/options.0.res.oracle
index 11d3288..a978dd2 100644
--- a/tests/meta-wp/oracle/options.0.res.oracle
+++ b/tests/meta-wp/oracle/options.0.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/meta-wp/options.c (with preprocessing)
+[kernel] Parsing options.c (with preprocessing)
[meta] Translation is enabled
[meta] Will process 5 properties
[meta] Successful translation
diff --git a/tests/meta-wp/oracle/options.1.res.oracle b/tests/meta-wp/oracle/options.1.res.oracle
index b0b2549..5b54128 100644
--- a/tests/meta-wp/oracle/options.1.res.oracle
+++ b/tests/meta-wp/oracle/options.1.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/meta-wp/options.c (with preprocessing)
+[kernel] Parsing options.c (with preprocessing)
[meta] Translation is enabled
[meta] Will process 5 properties
[meta] Successful translation
diff --git a/tests/meta-wp/oracle/pre_label.res.oracle b/tests/meta-wp/oracle/pre_label.res.oracle
index e2fb95b..ded678b 100644
--- a/tests/meta-wp/oracle/pre_label.res.oracle
+++ b/tests/meta-wp/oracle/pre_label.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/meta-wp/pre_label.c (with preprocessing)
+[kernel] Parsing pre_label.c (with preprocessing)
[meta] Translation is enabled
[meta] Will process 1 properties
[meta] Successful translation
diff --git a/tests/meta-wp/oracle/typing.res.oracle b/tests/meta-wp/oracle/typing.res.oracle
index 38ba0cd..2b436e5 100644
--- a/tests/meta-wp/oracle/typing.res.oracle
+++ b/tests/meta-wp/oracle/typing.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/meta-wp/typing.c (with preprocessing)
+[kernel] Parsing typing.c (with preprocessing)
[meta] Translation is enabled
[meta] Will process 1 properties
[meta] Successful translation
@@ -14,7 +14,7 @@
Function f
------------------------------------------------------------
-Goal Assertion 'test,meta' (file tests/meta-wp/typing.c, line 22):
+Goal Assertion 'test,meta' (file typing.c, line 22):
Assume {
(* Heap *)
Type: (region(s_1.base) <= 0) /\ (region(t.base) <= 0) /\
@@ -32,7 +32,7 @@ Prover Alt-Ergo returns Valid
------------------------------------------------------------
-Goal Assigns (file tests/meta-wp/typing.c, line 15) in 'f':
+Goal Assigns (file typing.c, line 15) in 'f':
Effect at line 18
Let a = shiftfield_F4_S_a(s).
Assume {
@@ -54,7 +54,7 @@ Prove: a = shiftfield_F4_S_a(s_1).
Prover Qed returns Valid
------------------------------------------------------------
-[wp] tests/meta-wp/typing.c:17: Warning:
+[wp] typing.c:17: Warning:
Memory model hypotheses for function 'f':
/*@
behavior wp_typed:
diff --git a/tests/meta-wp/oracle/uncalled.res.oracle b/tests/meta-wp/oracle/uncalled.res.oracle
index 9c0a5ac..ea32840 100644
--- a/tests/meta-wp/oracle/uncalled.res.oracle
+++ b/tests/meta-wp/oracle/uncalled.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/meta-wp/uncalled.c (with preprocessing)
+[kernel] Parsing uncalled.c (with preprocessing)
[meta] Translation is enabled
[meta] Will process 2 properties
[meta] Warning: \called_arg cannot be used with indirect calls
diff --git a/tests/meta/oracle/absent.0.res.oracle b/tests/meta/oracle/absent.0.res.oracle
index 6f86734..f1f8bcb 100644
--- a/tests/meta/oracle/absent.0.res.oracle
+++ b/tests/meta/oracle/absent.0.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/meta/absent.c (with preprocessing)
+[kernel] Parsing absent.c (with preprocessing)
[meta] Translation is enabled
[meta] Will process 2 properties
[meta] Successful translation
diff --git a/tests/meta/oracle/absent.1.res.oracle b/tests/meta/oracle/absent.1.res.oracle
index d81fbc5..9fc16be 100644
--- a/tests/meta/oracle/absent.1.res.oracle
+++ b/tests/meta/oracle/absent.1.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/meta/absent.c (with preprocessing)
+[kernel] Parsing absent.c (with preprocessing)
[meta] Translation is enabled
[meta] Will process 2 properties
[meta:unknown-func] Warning:
diff --git a/tests/meta/oracle/bindings_test.res.oracle b/tests/meta/oracle/bindings_test.res.oracle
index b6cbd1d..f28d875 100644
--- a/tests/meta/oracle/bindings_test.res.oracle
+++ b/tests/meta/oracle/bindings_test.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/meta/bindings_test.c (with preprocessing)
+[kernel] Parsing bindings_test.c (with preprocessing)
[meta] Translation is enabled
[meta] Will process 1 properties
[meta] Successful translation
diff --git a/tests/meta/oracle/called_arg.res.oracle b/tests/meta/oracle/called_arg.res.oracle
index 4b876aa..3c5f0a8 100644
--- a/tests/meta/oracle/called_arg.res.oracle
+++ b/tests/meta/oracle/called_arg.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/meta/called_arg.c (with preprocessing)
+[kernel] Parsing called_arg.c (with preprocessing)
[meta] Translation is enabled
[meta] Will process 2 properties
[meta] Successful translation
diff --git a/tests/meta/oracle/callees.res.oracle b/tests/meta/oracle/callees.res.oracle
index 97c0764..f28bac4 100644
--- a/tests/meta/oracle/callees.res.oracle
+++ b/tests/meta/oracle/callees.res.oracle
@@ -1,5 +1,5 @@
-[kernel] Parsing tests/meta/callees.c (with preprocessing)
-[kernel:typing:implicit-function-declaration] tests/meta/callees.c:5: Warning:
+[kernel] Parsing callees.c (with preprocessing)
+[kernel:typing:implicit-function-declaration] callees.c:5: Warning:
Calling undeclared function c. Old style K&R code?
[meta] Translation is enabled
[meta] Will process 1 properties
diff --git a/tests/meta/oracle/func_meta_var.res.oracle b/tests/meta/oracle/func_meta_var.res.oracle
index e7a707d..6515725 100644
--- a/tests/meta/oracle/func_meta_var.res.oracle
+++ b/tests/meta/oracle/func_meta_var.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/meta/func_meta_var.i (no preprocessing)
+[kernel] Parsing func_meta_var.i (no preprocessing)
[meta] Translation is enabled
[meta] Will process 1 properties
[meta] Successful translation
diff --git a/tests/meta/oracle/named.res.oracle b/tests/meta/oracle/named.res.oracle
index e5f9070..a5b015e 100644
--- a/tests/meta/oracle/named.res.oracle
+++ b/tests/meta/oracle/named.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/meta/named.c (with preprocessing)
+[kernel] Parsing named.c (with preprocessing)
[meta] Translation is enabled
[meta] Will process 1 properties
[meta] Successful translation
diff --git a/tests/meta/oracle/number_assertions.0.res.oracle b/tests/meta/oracle/number_assertions.0.res.oracle
index faedd18..7c0414b 100644
--- a/tests/meta/oracle/number_assertions.0.res.oracle
+++ b/tests/meta/oracle/number_assertions.0.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/meta/number_assertions.c (with preprocessing)
+[kernel] Parsing number_assertions.c (with preprocessing)
[meta] Translation is enabled
[meta] Will process 3 properties
[meta] Successful translation
diff --git a/tests/meta/oracle/passthrough.res.oracle b/tests/meta/oracle/passthrough.res.oracle
index a9b6b4d..f3f8b69 100644
--- a/tests/meta/oracle/passthrough.res.oracle
+++ b/tests/meta/oracle/passthrough.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/meta/passthrough.c (with preprocessing)
+[kernel] Parsing passthrough.c (with preprocessing)
[meta] Translation is enabled
[meta] Will process 2 properties
[meta] Successful translation
diff --git a/tests/meta/oracle/quantif.res.oracle b/tests/meta/oracle/quantif.res.oracle
index 3cd9292..407e599 100644
--- a/tests/meta/oracle/quantif.res.oracle
+++ b/tests/meta/oracle/quantif.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/meta/quantif.c (with preprocessing)
+[kernel] Parsing quantif.c (with preprocessing)
[meta] Translation is enabled
[meta] Will process 1 properties
[meta] Successful translation
diff --git a/tests/meta/oracle/read_addrof.res.oracle b/tests/meta/oracle/read_addrof.res.oracle
index 5d7338a..93b98bb 100644
--- a/tests/meta/oracle/read_addrof.res.oracle
+++ b/tests/meta/oracle/read_addrof.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/meta/read_addrof.i (no preprocessing)
+[kernel] Parsing read_addrof.i (no preprocessing)
[meta] Translation is enabled
[meta] Will process 1 properties
[meta] Successful translation
diff --git a/tests/meta/oracle/renaming.res.oracle b/tests/meta/oracle/renaming.res.oracle
index 394669c..95cec8a 100644
--- a/tests/meta/oracle/renaming.res.oracle
+++ b/tests/meta/oracle/renaming.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/meta/renaming.c (with preprocessing)
+[kernel] Parsing renaming.c (with preprocessing)
[meta] Translation is enabled
[meta] Will process 1 properties
[meta] Successful translation
diff --git a/tests/meta/oracle/simplify.res.oracle b/tests/meta/oracle/simplify.res.oracle
index 58671ad..7ffb11c 100644
--- a/tests/meta/oracle/simplify.res.oracle
+++ b/tests/meta/oracle/simplify.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/meta/simplify.c (with preprocessing)
+[kernel] Parsing simplify.c (with preprocessing)
[meta] Translation is enabled
[meta] Will process 2 properties
[meta] Successful translation
diff --git a/tests/meta/oracle/temp_variables.res.oracle b/tests/meta/oracle/temp_variables.res.oracle
index f2e20c1..42e282c 100644
--- a/tests/meta/oracle/temp_variables.res.oracle
+++ b/tests/meta/oracle/temp_variables.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/meta/temp_variables.c (with preprocessing)
+[kernel] Parsing temp_variables.c (with preprocessing)
[meta] Translation is enabled
[meta] Will process 1 properties
[meta] Successful translation
diff --git a/tests/meta/oracle/unspecified_sequence.res.oracle b/tests/meta/oracle/unspecified_sequence.res.oracle
index 918b1e0..f26ec20 100644
--- a/tests/meta/oracle/unspecified_sequence.res.oracle
+++ b/tests/meta/oracle/unspecified_sequence.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/meta/unspecified_sequence.c (with preprocessing)
+[kernel] Parsing unspecified_sequence.c (with preprocessing)
[meta] Translation is enabled
[meta] Will process 2 properties
[meta] Successful translation
--
GitLab