update oracles according to Value's changes

src/plugins/e-acsl/tests/e-acsl-runtime/oracle/loop.res.oracle

@@ -49,8 +49,8 @@ tests/e-acsl-runtime/loop.i:21:[kernel] warning: completely indeterminate value
 tests/e-acsl-runtime/loop.i:21:[kernel] warning: completely indeterminate value in t with offsets [3360..3808],0%32.
 tests/e-acsl-runtime/loop.i:21:[kernel] warning: completely indeterminate value in t with offsets [3840..4288],0%32.
 tests/e-acsl-runtime/loop.i:21:[kernel] warning: completely indeterminate value in t with offsets [4320..4768],0%32.
-tests/e-acsl-runtime/loop.i:21:[value] all evaluations are invalid for function call argument
-        (long)t[__e_acsl_k_2][__e_acsl_l_2]
+tests/e-acsl-runtime/loop.i:21:[value] completely invalid value in evaluation of
+        argument (long)t[__e_acsl_k_2][__e_acsl_l_2]
 [value] using specification for function __gmpz_add
 FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:143:[value] Function __gmpz_add: precondition got status valid.
 FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:144:[value] Function __gmpz_add: precondition got status valid.

src/plugins/e-acsl/tests/e-acsl-runtime/oracle/mainargs.1.res.oracle

@@ -68,7 +68,6 @@ tests/e-acsl-runtime/mainargs.c:18:[value] Assertion got status unknown.
 [value] using specification for function __initialized
 tests/e-acsl-runtime/mainargs.c:18:[kernel] warning: out of bounds read. assert \valid_read(argv+(long)argc);
 tests/e-acsl-runtime/mainargs.c:19:[value] entering loop for the first time
-tests/e-acsl-runtime/mainargs.c:20:[kernel] warning: out of bounds read. assert \valid_read(argv+i);
 FRAMAC_SHARE/libc/string.h:86:[value] Function __e_acsl_strlen: precondition 'valid_string_src' got status unknown.
 [value] using specification for function strlen
 FRAMAC_SHARE/libc/string.h:86:[value] Function strlen: precondition 'valid_string_src' got status unknown.
@@ -76,11 +75,8 @@ FRAMAC_SHARE/libc/string.h:90:[value] cannot evaluate ACSL term, unsupported ACS
 [value] using specification for function __delete_block
 FRAMAC_SHARE/libc/string.h:88:[value] Function __e_acsl_strlen: postcondition got status unknown.
 tests/e-acsl-runtime/mainargs.c:21:[value] Assertion got status unknown.
-tests/e-acsl-runtime/mainargs.c:21:[kernel] warning: out of bounds read. assert \valid_read(argv+(long)i);
 tests/e-acsl-runtime/mainargs.c:22:[value] Assertion got status unknown.
 tests/e-acsl-runtime/mainargs.c:22:[value] entering loop for the first time
-tests/e-acsl-runtime/mainargs.c:22:[kernel] warning: out of bounds read. assert \valid_read(argv+(long)i);
-tests/e-acsl-runtime/mainargs.c:19:[kernel] warning: signed overflow. assert i+1 ≤ 2147483647;
 [value] using specification for function __e_acsl_memory_clean
 [value] done for function main
 [value] ====== VALUES COMPUTED ======

src/plugins/e-acsl/tests/e-acsl-runtime/oracle/mainargs.res.oracle

@@ -44,7 +44,6 @@ tests/e-acsl-runtime/mainargs.c:18:[value] Assertion got status unknown.
 [value] using specification for function __initialized
 tests/e-acsl-runtime/mainargs.c:18:[kernel] warning: out of bounds read. assert \valid_read(argv+argc);
 tests/e-acsl-runtime/mainargs.c:19:[value] entering loop for the first time
-tests/e-acsl-runtime/mainargs.c:20:[kernel] warning: out of bounds read. assert \valid_read(argv+i);
 FRAMAC_SHARE/libc/string.h:86:[value] Function __e_acsl_strlen: precondition 'valid_string_src' got status unknown.
 [value] using specification for function strlen
 FRAMAC_SHARE/libc/string.h:86:[value] Function strlen: precondition 'valid_string_src' got status unknown.
@@ -52,10 +51,8 @@ FRAMAC_SHARE/libc/string.h:90:[value] cannot evaluate ACSL term, unsupported ACS
 [value] using specification for function __delete_block
 FRAMAC_SHARE/libc/string.h:88:[value] Function __e_acsl_strlen: postcondition got status unknown.
 tests/e-acsl-runtime/mainargs.c:21:[value] Assertion got status unknown.
-tests/e-acsl-runtime/mainargs.c:21:[kernel] warning: out of bounds read. assert \valid_read(argv+i);
 tests/e-acsl-runtime/mainargs.c:22:[value] Assertion got status unknown.
 tests/e-acsl-runtime/mainargs.c:22:[value] entering loop for the first time
-tests/e-acsl-runtime/mainargs.c:22:[kernel] warning: out of bounds read. assert \valid_read(argv+i);
 [value] using specification for function __e_acsl_memory_clean
 [value] done for function main
 [value] ====== VALUES COMPUTED ======

src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.1.res.oracle

@@ -71,8 +71,8 @@ FRAMAC_SHARE/libc/stdlib.h:177:[value] Function __e_acsl_free, behavior dealloca
 tests/e-acsl-runtime/valid.c:49:[value] Assertion got status valid.
 tests/e-acsl-runtime/valid.c:49:[kernel] warning: accessing left-value that contains escaping addresses: assert \specified(&a);
 tests/e-acsl-runtime/valid.c:49:[kernel] warning: completely indeterminate value in a.
-tests/e-acsl-runtime/valid.c:49:[value] all evaluations are invalid for function call argument
-        (void *)a
+tests/e-acsl-runtime/valid.c:49:[value] completely invalid value in evaluation of
+        argument (void *)a
 tests/e-acsl-runtime/valid.c:50:[value] Assertion got status valid.
 tests/e-acsl-runtime/valid.c:30:[value] Assertion got status valid.
 [value] using specification for function __e_acsl_memory_clean

src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.res.oracle

@@ -63,8 +63,8 @@ FRAMAC_SHARE/libc/stdlib.h:177:[value] Function __e_acsl_free, behavior dealloca
 tests/e-acsl-runtime/valid.c:49:[value] Assertion got status valid.
 tests/e-acsl-runtime/valid.c:49:[kernel] warning: accessing left-value that contains escaping addresses: assert \specified(&a);
 tests/e-acsl-runtime/valid.c:49:[kernel] warning: completely indeterminate value in a.
-tests/e-acsl-runtime/valid.c:49:[value] all evaluations are invalid for function call argument
-        (void *)a
+tests/e-acsl-runtime/valid.c:49:[value] completely invalid value in evaluation of
+        argument (void *)a
 tests/e-acsl-runtime/valid.c:50:[value] Assertion got status valid.
 tests/e-acsl-runtime/valid.c:30:[value] Assertion got status valid.
 [value] using specification for function __e_acsl_memory_clean

src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.1.res.oracle

@@ -60,12 +60,12 @@ FRAMAC_SHARE/libc/stdlib.h:177:[value] Function __e_acsl_free, behavior dealloca
 tests/e-acsl-runtime/valid_alias.c:19:[value] Assertion got status valid.
 tests/e-acsl-runtime/valid_alias.c:19:[kernel] warning: accessing left-value that contains escaping addresses: assert \specified(&a);
 tests/e-acsl-runtime/valid_alias.c:19:[kernel] warning: completely indeterminate value in a.
-tests/e-acsl-runtime/valid_alias.c:19:[value] all evaluations are invalid for function call argument
-        (void *)a
+tests/e-acsl-runtime/valid_alias.c:19:[value] completely invalid value in evaluation of
+        argument (void *)a
 tests/e-acsl-runtime/valid_alias.c:19:[kernel] warning: accessing left-value that contains escaping addresses: assert \specified(&b);
 tests/e-acsl-runtime/valid_alias.c:19:[kernel] warning: completely indeterminate value in b.
-tests/e-acsl-runtime/valid_alias.c:19:[value] all evaluations are invalid for function call argument
-        (void *)b
+tests/e-acsl-runtime/valid_alias.c:19:[value] completely invalid value in evaluation of
+        argument (void *)b
 [value] using specification for function __e_acsl_memory_clean
 [value] done for function main
 [value] ====== VALUES COMPUTED ======

src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.res.oracle

@@ -58,12 +58,12 @@ FRAMAC_SHARE/libc/stdlib.h:177:[value] Function __e_acsl_free, behavior dealloca
 tests/e-acsl-runtime/valid_alias.c:19:[value] Assertion got status valid.
 tests/e-acsl-runtime/valid_alias.c:19:[kernel] warning: accessing left-value that contains escaping addresses: assert \specified(&a);
 tests/e-acsl-runtime/valid_alias.c:19:[kernel] warning: completely indeterminate value in a.
-tests/e-acsl-runtime/valid_alias.c:19:[value] all evaluations are invalid for function call argument
-        (void *)a
+tests/e-acsl-runtime/valid_alias.c:19:[value] completely invalid value in evaluation of
+        argument (void *)a
 tests/e-acsl-runtime/valid_alias.c:19:[kernel] warning: accessing left-value that contains escaping addresses: assert \specified(&b);
 tests/e-acsl-runtime/valid_alias.c:19:[kernel] warning: completely indeterminate value in b.
-tests/e-acsl-runtime/valid_alias.c:19:[value] all evaluations are invalid for function call argument
-        (void *)b
+tests/e-acsl-runtime/valid_alias.c:19:[value] completely invalid value in evaluation of
+        argument (void *)b
 [value] using specification for function __e_acsl_memory_clean
 [value] done for function main
 [value] ====== VALUES COMPUTED ======

src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_in_contract.1.res.oracle

@@ -24,8 +24,8 @@
 [value] using specification for function e_acsl_assert
 FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
 tests/e-acsl-runtime/valid_in_contract.c:21:[kernel] warning: out of bounds read. assert \valid_read(&l->next);
-tests/e-acsl-runtime/valid_in_contract.c:21:[value] all evaluations are invalid for function call argument
-        (void *)l->next
+tests/e-acsl-runtime/valid_in_contract.c:21:[value] completely invalid value in evaluation of
+        argument (void *)l->next
 [value] using specification for function __full_init
 [value] using specification for function __delete_block
 tests/e-acsl-runtime/valid_in_contract.c:18:[value] Function f, behavior B1: postcondition got status valid.

src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_in_contract.res.oracle

@@ -24,8 +24,8 @@
 [value] using specification for function e_acsl_assert
 FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
 tests/e-acsl-runtime/valid_in_contract.c:21:[kernel] warning: out of bounds read. assert \valid_read(&l->next);
-tests/e-acsl-runtime/valid_in_contract.c:21:[value] all evaluations are invalid for function call argument
-        (void *)l->next
+tests/e-acsl-runtime/valid_in_contract.c:21:[value] completely invalid value in evaluation of
+        argument (void *)l->next
 [value] using specification for function __full_init
 [value] using specification for function __delete_block
 tests/e-acsl-runtime/valid_in_contract.c:18:[value] Function f, behavior B1: postcondition got status valid.