[Eva] Updates test oracles.

src/plugins/e-acsl/tests/arith/oracle_ci/at_on-purely-logic-variables.res.oracle

@@ -59,8 +59,6 @@
   function __e_acsl_assert: precondition got status unknown.
 [eva:alarm] tests/arith/at_on-purely-logic-variables.c:7: Warning: 
   function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/arith/at_on-purely-logic-variables.c:6: Warning: 
-  function __gen_e_acsl_f: postcondition got status unknown.
 [eva:alarm] tests/arith/at_on-purely-logic-variables.c:8: Warning: 
   function __gen_e_acsl_f: postcondition got status unknown.
 [eva:alarm] tests/arith/at_on-purely-logic-variables.c:16: Warning: 

src/plugins/e-acsl/tests/arith/oracle_ci/quantif.res.oracle

 [e-acsl] beginning translation.
 [e-acsl] translation done in project "e-acsl".
-[eva:alarm] tests/arith/quantif.i:9: Warning: assertion got status unknown.
-[eva:alarm] tests/arith/quantif.i:10: Warning: assertion got status unknown.
-[eva:alarm] tests/arith/quantif.i:11: Warning: assertion got status unknown.
 [eva:alarm] tests/arith/quantif.i:15: Warning: 
   function __e_acsl_assert: precondition got status unknown.
 [eva:alarm] tests/arith/quantif.i:15: Warning: assertion got status unknown.
@@ -12,14 +9,10 @@
 [eva:alarm] tests/arith/quantif.i:24: Warning: assertion got status unknown.
 [eva:alarm] tests/arith/quantif.i:30: Warning: 
   function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/arith/quantif.i:30: Warning: assertion got status unknown.
 [eva:alarm] tests/arith/quantif.i:31: Warning: 
   function __e_acsl_assert: precondition got status unknown.
 [eva:alarm] tests/arith/quantif.i:32: Warning: 
   function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/arith/quantif.i:32: Warning: assertion got status unknown.
 [eva:alarm] tests/arith/quantif.i:33: Warning: 
   function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/arith/quantif.i:33: Warning: assertion got status unknown.
-[eva:alarm] tests/arith/quantif.i:37: Warning: assertion got status unknown.
 [eva:alarm] tests/arith/quantif.i:40: Warning: assertion got status unknown.

src/plugins/e-acsl/tests/examples/oracle_ci/linear_search.res.oracle

@@ -4,10 +4,10 @@
   function __gen_e_acsl_search: precondition got status unknown.
 [eva:alarm] tests/examples/linear_search.i:7: Warning: 
   function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/examples/linear_search.i:18: Warning: 
-  loop invariant got status unknown.
 [eva:alarm] tests/examples/linear_search.i:18: Warning: 
   function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/examples/linear_search.i:18: Warning: 
+  loop invariant got status unknown.
 [eva:alarm] tests/examples/linear_search.i:10: Warning: 
   function __e_acsl_assert: precondition got status unknown.
 [eva:alarm] tests/examples/linear_search.i:13: Warning: 

tests/libc/oracle/string_c.res.oracle

@@ -769,8 +769,9 @@
   function memchr, behavior found: postcondition 'result_same_base' got status valid. (Behavior may be inactive, no reduction performed.)
 [eva] share/libc/string.h:80: 
   function memchr, behavior found: postcondition 'result_char' got status valid. (Behavior may be inactive, no reduction performed.)
-[eva:alarm] share/libc/string.h:81: Warning: 
-  function memchr, behavior found: postcondition 'result_in_str' got status unknown. (Behavior may be inactive, no reduction performed.)
+[kernel] share/libc/string.c:248: Warning: using size of 'void'
+[eva] share/libc/string.h:81: 
+  function memchr, behavior found: postcondition 'result_in_str' got status valid. (Behavior may be inactive, no reduction performed.)
 [eva:alarm] share/libc/string.h:86: Warning: 
   function memchr, behavior not_found: postcondition 'result_null' got status invalid. (Behavior may be inactive, no reduction performed.)
 [eva] Recording results for memchr
@@ -801,6 +802,8 @@
   function memchr: precondition 'initialization' got status valid.
 [eva] tests/libc/string_c.c:231: 
   function memchr: precondition 'danglingness' got status valid.
+[eva:alarm] share/libc/string.h:81: Warning: 
+  function memchr, behavior found: postcondition 'result_in_str' got status unknown. (Behavior may be inactive, no reduction performed.)
 [eva] Recording results for memchr
 [eva] Done for function memchr
 [eva] tests/libc/string_c.c:232: assertion got status valid.

tests/value/oracle/forall.res.oracle

@@ -8,7 +8,7 @@
 [eva:alarm] tests/value/forall.i:9: Warning: 
   function main: precondition got status unknown.
 [eva] tests/value/forall.i:11: assertion got status valid.
-[eva:alarm] tests/value/forall.i:12: Warning: assertion got status unknown.
+[eva] tests/value/forall.i:12: assertion got status valid.
 [eva] tests/value/forall.i:13: assertion got status valid.
 [eva:alarm] tests/value/forall.i:15: Warning: assertion got status unknown.
 [eva:alarm] tests/value/forall.i:16: Warning: assertion got status unknown.