[Eva] Updates test oracles.

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

@@ -3,7 +3,6 @@
 [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.
-[eva:alarm] tests/arith/quantif.i:20: Warning: assertion got status unknown.
 [eva:alarm] tests/arith/quantif.i:24: Warning: 
   function __e_acsl_assert: precondition got status unknown.
 [eva:alarm] tests/arith/quantif.i:24: Warning: assertion got status unknown.

tests/builtins/oracle/strchr.res.oracle

@@ -23,6 +23,8 @@
 [eva] tests/builtins/strchr.c:88: Call to builtin strchr
 [eva] tests/builtins/strchr.c:88: 
   function strchr: precondition 'valid_string_s' got status valid.
+[eva] share/libc/string.h:165: 
+  cannot evaluate ACSL term, unsupported logic var p
 [eva] tests/builtins/strchr.c:88: Frama_C_show_each_mystrchr: {3}
 [eva] tests/builtins/strchr.c:89: assertion got status valid.
 [eva] tests/builtins/strchr.c:92: Call to builtin strchr

tests/libc/oracle/stdlib_c_env.res.oracle

@@ -9,6 +9,8 @@
 [eva] share/libc/stdlib.c:114: Call to builtin strchr
 [eva] share/libc/stdlib.c:114: 
   function strchr: precondition 'valid_string_s' got status valid.
+[eva] share/libc/string.h:165: 
+  cannot evaluate ACSL term, unsupported logic var p
 [eva] share/libc/stdlib.c:115: 
   assertion 'string_contains_separator' got status valid.
 [eva] share/libc/stdlib.c:116: assertion 'name_is_not_empty' got status valid.

tests/libc/oracle/string_c.res.oracle

@@ -668,6 +668,8 @@
   function strchr, behavior found: postcondition 'result_in_length' got status valid.
 [eva] share/libc/string.h:164: 
   function strchr, behavior found: postcondition 'result_valid_string' got status valid.
+[eva] share/libc/string.h:165: 
+  cannot evaluate ACSL term, unsupported logic var p
 [eva:alarm] share/libc/string.h:165: Warning: 
   function strchr, behavior found: postcondition 'result_first_occur' got status unknown.
 [eva] share/libc/string.h:171: 

tests/libc/oracle/string_c_generic.res.oracle

@@ -288,6 +288,8 @@
   function strchr, behavior found: postcondition 'result_in_length' got status valid.
 [eva] share/libc/string.h:164: 
   function strchr, behavior found: postcondition 'result_valid_string' got status valid.
+[eva] share/libc/string.h:165: 
+  cannot evaluate ACSL term, unsupported logic var p
 [eva:alarm] share/libc/string.h:165: Warning: 
   function strchr, behavior found: postcondition 'result_first_occur' got status unknown.
 [eva] share/libc/string.h:171: 

tests/libc/oracle/string_c_strchr.res.oracle

@@ -67,6 +67,8 @@
   function strchr, behavior found: postcondition 'result_in_length' got status valid.
 [eva] share/libc/string.h:164: 
   function strchr, behavior found: postcondition 'result_valid_string' got status valid.
+[eva] share/libc/string.h:165: 
+  cannot evaluate ACSL term, unsupported logic var p
 [eva:alarm] share/libc/string.h:165: Warning: 
   function strchr, behavior found: postcondition 'result_first_occur' got status unknown.
 [eva] Recording results for strchr

tests/libc/oracle/string_h.res.oracle

@@ -143,12 +143,8 @@
 [eva] tests/libc/string_h.c:75: 
   function strtok: precondition 'valid_string_delim' got status valid.
 [eva:alarm] tests/libc/string_h.c:75: Warning: 
-  function strtok, behavior new_str: precondition 'valid_string_s_or_delim_not_found' got status unknown.
-[eva:invalid-assigns] tests/libc/string_h.c:75: 
-  Completely invalid destination for assigns clause *(s + (0 ..)). Ignoring.
+  function strtok, behavior new_str: precondition 'valid_string_s_or_delim_not_found' got status invalid.
 [eva] Done for function strtok
-[eva:alarm] tests/libc/string_h.c:76: Warning: 
-  assertion 'unreachable_if_precise' got status invalid (stopping propagation).
 [eva] Recording results for test_strtok
 [eva] Done for function test_strtok
 [eva] computing for function test_strtok_r <- main.
@@ -232,12 +228,8 @@
 [eva] tests/libc/string_h.c:105: 
   function strtok_r: precondition 'valid_saveptr' got status valid.
 [eva:alarm] tests/libc/string_h.c:105: Warning: 
-  function strtok_r, behavior new_str: precondition 'valid_string_s_or_delim_not_found' got status unknown.
-[eva:invalid-assigns] tests/libc/string_h.c:105: 
-  Completely invalid destination for assigns clause *(s + (0 ..)). Ignoring.
+  function strtok_r, behavior new_str: precondition 'valid_string_s_or_delim_not_found' got status invalid.
 [eva] Done for function strtok_r
-[eva:alarm] tests/libc/string_h.c:106: Warning: 
-  assertion 'unreachable_if_precise' got status invalid (stopping propagation).
 [eva] Recording results for test_strtok_r
 [eva] Done for function test_strtok_r
 [eva] computing for function strdup <- main.
@@ -333,6 +325,8 @@
 [eva] tests/libc/string_h.c:154: Call to builtin strchr
 [eva] tests/libc/string_h.c:154: 
   function strchr: precondition 'valid_string_s' got status valid.
+[eva] share/libc/string.h:165: 
+  cannot evaluate ACSL term, unsupported logic var p
 [eva] computing for function strchrnul <- main.
   Called from tests/libc/string_h.c:155.
 [eva] using specification for function strchrnul

tests/value/oracle/annot_valid.res.oracle

@@ -17,7 +17,7 @@
 [eva:alarm] tests/value/annot_valid.i:29: Warning: assertion got status unknown.
 [eva:alarm] tests/value/annot_valid.i:32: Warning: assertion got status unknown.
 [eva:alarm] tests/value/annot_valid.i:35: Warning: assertion got status unknown.
-[eva:alarm] tests/value/annot_valid.i:38: Warning: assertion got status unknown.
+[eva] tests/value/annot_valid.i:38: assertion got status valid.
 [eva] tests/value/annot_valid.i:41: assertion got status valid.
 [eva:alarm] tests/value/annot_valid.i:44: Warning: 
   assertion got status invalid (stopping propagation).