[Tests] oracle updates

tests/meta-deduce/oracle/consequence.res.oracle

-[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

tests/meta-deduce/oracle/deduction_with_offset.res.oracle

-[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

tests/meta-deduce/oracle/negative_assigns.res.oracle

-[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

tests/meta-wp/oracle/assert_type_of.res.oracle

-[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

tests/meta-wp/oracle/axiomatic_requires.res.oracle

-[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

tests/meta-wp/oracle/dummy.res.oracle

-[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); */

tests/meta-wp/oracle/forbidden.res.oracle

-[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

tests/meta-wp/oracle/invariant.res.oracle

-[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;
 }
 

tests/meta-wp/oracle/loop_invariant.res.oracle

-[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

tests/meta-wp/oracle/monotony.res.oracle

-[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

tests/meta-wp/oracle/options.0.res.oracle

-[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

tests/meta-wp/oracle/options.1.res.oracle

-[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

tests/meta-wp/oracle/pre_label.res.oracle

-[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

tests/meta-wp/oracle/typing.res.oracle

-[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:

tests/meta-wp/oracle/uncalled.res.oracle

-[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

tests/meta/oracle/absent.0.res.oracle

-[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

tests/meta/oracle/absent.1.res.oracle

-[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: 

tests/meta/oracle/bindings_test.res.oracle

-[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

tests/meta/oracle/called_arg.res.oracle

-[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

tests/meta/oracle/callees.res.oracle

-[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