diff --git a/tests/meta-deduce/oracle/consequence.res.oracle b/tests/meta-deduce/oracle/consequence.res.oracle
index 20cb730b7dfda06cf2bf82d802da76fab34401d7..5ce7fbdb3d220c48717b3c4d03895406c3120d4b 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 a5f42908d18dfb0530607a303d6c5b04ecef1b90..6c45864c4f66fa8e733b3e80367519262cca3d49 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 43ea6cd46aef507138c38b50907b51d3271d4b78..9321887c3cd9e073996c9814a0a5587e088b5253 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 43fdbdcbbf3b83622a5fea4d55714f2a61e24de5..fdc43b1d7e435a6dd546cc3572f6c9be00374bdd 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 03f1412e43822423a705b833e3520a0b089bb0eb..db2ced85936338eb1cdac960d93b8850d40cbbe3 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 ec1cf8fcec4e8392648ffd3a94281519e0d3a5ef..358bcc5e952952639aa0e5b18a39e931969c98a8 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 3a7e4d858cde01672d4ebba932e487dc3f3f4da5..3c5e6584da39a9cb5b00c3857cb00d2cceb0bede 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 2cf5a2c3919cd060e3899f62736659055b35dd3c..13970de12a69010e144b74ec648527e8726f9835 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 dd9cf161f8403d3225dfbc41289ba7abcfde2ae0..320b858e4bb71d83eefde7e95b07f9dfa0b77850 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 9c2212d3e7b7e29fc994e59fa4d974f1721f1aa9..0afaf534690865ec46f0c2b7b132b98c03998b76 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 11d3288a19e90021c8b4de1a3648cba806a4f7b3..a978dd22c3ebac324019e0dc41d8c7466ccc7fd2 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 b0b2549773ac50ae4b18b8c91d77e1b126844059..5b541280dc0c1695f69c8449ccb8dbe8bbea0ffb 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 e2fb95b05c11be01ff0ca02739b0da6d70700072..ded678be98ac6690de699c574fd9fa3b3a4ce757 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 38ba0cdf3669484a990b1ca65ab4ef7b977e33c8..2b436e5d42600df0ba103943b6b2851a316a7ba9 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 9c0a5ac6ed930c8788815d00fe61e54bfda21a9d..ea32840f074daf5a5fe1be88dd670f5eb3783837 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 6f867341bd881bc61859d64761336b54bccfe07b..f1f8bcb621706a34b03e2072fd91d1e4535e99f0 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 d81fbc5da58b666d79eca87abb8ff1c639682954..9fc16bee2c83aa0ab2f5d00ae6a230c1ba886140 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 b6cbd1d1cd9f20e6aa10222c374880f060bdc6d8..f28d8758f4339b556dc5f8cde5bb29b04684e24c 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 4b876aa213ac67398d489a38e659dc7222be1d17..3c5f0a889aa02e9258d4ac2c4fa3acc08185d0d0 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 97c07648af622a0c0325305485f0df26e0cf8703..f28bac473b73cb6510173beaf85bb89144c8a80a 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 e7a707d6665b56d6f8b3873d6f8ba6ada650d847..651572578ed8584816e92485ddc56561b89a6441 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 e5f9070b802f2c2c5bc6b1eb679951f4f351fc24..a5b015ed1ee382f18b05ba1294d9862be63afc4b 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 faedd18e6598ebf591ab837f14905a3656d61350..7c0414b4cddaeebfa3e8611651681ff24a73dfd9 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 a9b6b4d1bf9d27df7f3319c567e89f66ec921d1b..f3f8b69ddaed82081b56f2848c0bdc196c347ad6 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 3cd9292998061a338dad1856516947762f764f40..407e599268c364c5463f55997619fd0c568b0954 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 5d7338acee4d96091331fd2c94f74e1a827678ac..93b98bb34ca3a8cde6d23fa6f171bc4f2c22975b 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 394669c71ab3fcb1347866c32762197ddb8bf7f2..95cec8aba9ad7c3fed199a2600ab5e2982798776 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 58671ad74ea85006b1acddf765712982069a4e83..7ffb11c6183ba51fe09a3d31eac1e772aafa041a 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 f2e20c1a6cc526810096e8937f44fe6d09992c4c..42e282c5e496299ac7080b8817048612a7394ef1 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 918b1e0911dccebabb74177a3469e481ba9fd0c2..f26ec20b9395f5484ea6ecba07659d0370e44cec 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