[E-ACSL] update oracles according to Value's changes

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

@@ -47,11 +47,9 @@ tests/e-acsl-runtime/bts1324.i:8:[kernel] warning: out of bounds read. assert \v
 tests/e-acsl-runtime/bts1324.i:15:[value] entering loop for the first time
 [value] using specification for function __delete_block
 tests/e-acsl-runtime/bts1324.i:9:[value] Function sorted, behavior yes: postcondition got status valid.
-tests/e-acsl-runtime/bts1324.i:9:[value] Function sorted, behavior yes: postcondition got status valid, but it is unknown if the behavior is active.
 [value] using specification for function e_acsl_assert
 ./share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
 tests/e-acsl-runtime/bts1324.i:9:[value] Function __e_acsl_sorted, behavior yes: postcondition got status valid.
-tests/e-acsl-runtime/bts1324.i:9:[value] Function __e_acsl_sorted, behavior yes: postcondition got status valid, but it is unknown if the behavior is active.
 tests/e-acsl-runtime/bts1324.i:25:[value] Assertion got status valid.
 [value] using specification for function __clean
 [kernel] warning: Neither code nor specification for function __clean, generating default assigns from the prototype

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

@@ -21,10 +21,8 @@
 tests/e-acsl-runtime/bts1324.i:15:[value] entering loop for the first time
 [value] using specification for function __delete_block
 tests/e-acsl-runtime/bts1324.i:9:[value] Function sorted, behavior yes: postcondition got status valid.
-tests/e-acsl-runtime/bts1324.i:9:[value] Function sorted, behavior yes: postcondition got status valid, but it is unknown if the behavior is active.
 ./share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
 tests/e-acsl-runtime/bts1324.i:9:[value] Function __e_acsl_sorted, behavior yes: postcondition got status valid.
-tests/e-acsl-runtime/bts1324.i:9:[value] Function __e_acsl_sorted, behavior yes: postcondition got status valid, but it is unknown if the behavior is active.
 tests/e-acsl-runtime/bts1324.i:25:[value] Assertion got status valid.
 [value] using specification for function __clean
 [kernel] warning: Neither code nor specification for function __clean, generating default assigns from the prototype

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

@@ -53,10 +53,10 @@ tests/e-acsl-runtime/function_contract.i:30:[value] Function j, behavior b1: pos
 tests/e-acsl-runtime/function_contract.i:34:[value] Function j, behavior b2: postcondition got status valid.
 tests/e-acsl-runtime/function_contract.i:30:[value] Function __e_acsl_j, behavior b1: postcondition got status valid.
 tests/e-acsl-runtime/function_contract.i:34:[value] Function __e_acsl_j, behavior b2: postcondition got status valid.
-tests/e-acsl-runtime/function_contract.i:40:[value] Function __e_acsl_k, behavior b1: assumption got status invalid; precondition not evaluated.
+tests/e-acsl-runtime/function_contract.i:40:[value] Function __e_acsl_k, behavior b1: behavior 'assumes' got status invalid; precondition not evaluated.
 tests/e-acsl-runtime/function_contract.i:44:[value] Function __e_acsl_k, behavior b2: precondition got status valid.
 tests/e-acsl-runtime/function_contract.i:45:[value] Function __e_acsl_k, behavior b2: precondition got status valid.
-tests/e-acsl-runtime/function_contract.i:40:[value] Function k, behavior b1: assumption got status invalid; precondition not evaluated.
+tests/e-acsl-runtime/function_contract.i:40:[value] Function k, behavior b1: behavior 'assumes' got status invalid; precondition not evaluated.
 tests/e-acsl-runtime/function_contract.i:44:[value] Function k, behavior b2: precondition got status valid.
 tests/e-acsl-runtime/function_contract.i:45:[value] Function k, behavior b2: precondition got status valid.
 tests/e-acsl-runtime/function_contract.i:51:[value] Assertion got status valid.

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

@@ -37,10 +37,10 @@ tests/e-acsl-runtime/function_contract.i:30:[value] Function j, behavior b1: pos
 tests/e-acsl-runtime/function_contract.i:34:[value] Function j, behavior b2: postcondition got status valid.
 tests/e-acsl-runtime/function_contract.i:30:[value] Function __e_acsl_j, behavior b1: postcondition got status valid.
 tests/e-acsl-runtime/function_contract.i:34:[value] Function __e_acsl_j, behavior b2: postcondition got status valid.
-tests/e-acsl-runtime/function_contract.i:40:[value] Function __e_acsl_k, behavior b1: assumption got status invalid; precondition not evaluated.
+tests/e-acsl-runtime/function_contract.i:40:[value] Function __e_acsl_k, behavior b1: behavior 'assumes' got status invalid; precondition not evaluated.
 tests/e-acsl-runtime/function_contract.i:44:[value] Function __e_acsl_k, behavior b2: precondition got status valid.
 tests/e-acsl-runtime/function_contract.i:45:[value] Function __e_acsl_k, behavior b2: precondition got status valid.
-tests/e-acsl-runtime/function_contract.i:40:[value] Function k, behavior b1: assumption got status invalid; precondition not evaluated.
+tests/e-acsl-runtime/function_contract.i:40:[value] Function k, behavior b1: behavior 'assumes' got status invalid; precondition not evaluated.
 tests/e-acsl-runtime/function_contract.i:44:[value] Function k, behavior b2: precondition got status valid.
 tests/e-acsl-runtime/function_contract.i:45:[value] Function k, behavior b2: precondition got status valid.
 tests/e-acsl-runtime/function_contract.i:51:[value] Assertion got status valid.

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

@@ -53,13 +53,9 @@ tests/e-acsl-runtime/linear_search.i:19:[value] Loop invariant got status valid.
 tests/e-acsl-runtime/linear_search.i:20:[value] Loop invariant got status unknown.
 tests/e-acsl-runtime/linear_search.i:21:[value] entering loop for the first time
 tests/e-acsl-runtime/linear_search.i:12:[value] Function search, behavior exists: postcondition got status unknown.
-tests/e-acsl-runtime/linear_search.i:12:[value] Function search, behavior exists: postcondition got status unknown, but it is unknown if the behavior is active.
 tests/e-acsl-runtime/linear_search.i:15:[value] Function search, behavior not_exists: postcondition got status unknown.
-tests/e-acsl-runtime/linear_search.i:15:[value] Function search, behavior not_exists: postcondition got status unknown, but it is unknown if the behavior is active.
 tests/e-acsl-runtime/linear_search.i:12:[value] Function __e_acsl_search, behavior exists: postcondition got status unknown.
-tests/e-acsl-runtime/linear_search.i:12:[value] Function __e_acsl_search, behavior exists: postcondition got status unknown, but it is unknown if the behavior is active.
 tests/e-acsl-runtime/linear_search.i:15:[value] Function __e_acsl_search, behavior not_exists: postcondition got status unknown.
-tests/e-acsl-runtime/linear_search.i:15:[value] Function __e_acsl_search, behavior not_exists: postcondition got status unknown, but it is unknown if the behavior is active.
 tests/e-acsl-runtime/linear_search.i:33:[value] Assertion got status unknown.
 tests/e-acsl-runtime/linear_search.i:36:[value] Assertion got status unknown.
 [value] using specification for function __clean

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

@@ -25,13 +25,9 @@ tests/e-acsl-runtime/linear_search.i:19:[value] Loop invariant got status valid.
 tests/e-acsl-runtime/linear_search.i:20:[value] Loop invariant got status unknown.
 tests/e-acsl-runtime/linear_search.i:21:[value] entering loop for the first time
 tests/e-acsl-runtime/linear_search.i:12:[value] Function search, behavior exists: postcondition got status unknown.
-tests/e-acsl-runtime/linear_search.i:12:[value] Function search, behavior exists: postcondition got status unknown, but it is unknown if the behavior is active.
 tests/e-acsl-runtime/linear_search.i:15:[value] Function search, behavior not_exists: postcondition got status unknown.
-tests/e-acsl-runtime/linear_search.i:15:[value] Function search, behavior not_exists: postcondition got status unknown, but it is unknown if the behavior is active.
 tests/e-acsl-runtime/linear_search.i:12:[value] Function __e_acsl_search, behavior exists: postcondition got status unknown.
-tests/e-acsl-runtime/linear_search.i:12:[value] Function __e_acsl_search, behavior exists: postcondition got status unknown, but it is unknown if the behavior is active.
 tests/e-acsl-runtime/linear_search.i:15:[value] Function __e_acsl_search, behavior not_exists: postcondition got status unknown.
-tests/e-acsl-runtime/linear_search.i:15:[value] Function __e_acsl_search, behavior not_exists: postcondition got status unknown, but it is unknown if the behavior is active.
 tests/e-acsl-runtime/linear_search.i:33:[value] Assertion got status unknown.
 tests/e-acsl-runtime/linear_search.i:36:[value] Assertion got status unknown.
 [value] using specification for function __clean

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

@@ -22,9 +22,7 @@ tests/e-acsl-runtime/localvar.c:26:[e-acsl] warning: E-ACSL construct `logic fun
 [value] using specification for function __full_init
 [value] using specification for function __delete_block
 FRAMAC_SHARE/libc/stdlib.h:127:[value] Function __e_acsl_malloc, behavior allocation: postcondition got status unknown.
-FRAMAC_SHARE/libc/stdlib.h:127:[value] Function __e_acsl_malloc, behavior allocation: postcondition got status unknown, but it is unknown if the behavior is active.
 FRAMAC_SHARE/libc/stdlib.h:132:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid.
-FRAMAC_SHARE/libc/stdlib.h:132:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid, but it is unknown if the behavior is active.
 tests/e-acsl-runtime/localvar.c:20:[value] Assertion got status valid.
 [value] using specification for function __initialized
 ./share/e-acsl/memory_model/e_acsl_mmodel.h:85:[value] Function __initialized: postcondition got status unknown.

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

@@ -22,9 +22,7 @@ tests/e-acsl-runtime/localvar.c:26:[e-acsl] warning: E-ACSL construct `logic fun
 [value] using specification for function __full_init
 [value] using specification for function __delete_block
 FRAMAC_SHARE/libc/stdlib.h:127:[value] Function __e_acsl_malloc, behavior allocation: postcondition got status unknown.
-FRAMAC_SHARE/libc/stdlib.h:127:[value] Function __e_acsl_malloc, behavior allocation: postcondition got status unknown, but it is unknown if the behavior is active.
 FRAMAC_SHARE/libc/stdlib.h:132:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid.
-FRAMAC_SHARE/libc/stdlib.h:132:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid, but it is unknown if the behavior is active.
 tests/e-acsl-runtime/localvar.c:20:[value] Assertion got status valid.
 [value] using specification for function __initialized
 ./share/e-acsl/memory_model/e_acsl_mmodel.h:85:[value] Function __initialized: postcondition got status unknown.

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

@@ -40,9 +40,7 @@ tests/e-acsl-runtime/valid.c:27:[value] Non-termination in evaluation of functio
 ./share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
 [value] using specification for function __delete_block
 FRAMAC_SHARE/libc/stdlib.h:127:[value] Function __e_acsl_malloc, behavior allocation: postcondition got status unknown.
-FRAMAC_SHARE/libc/stdlib.h:127:[value] Function __e_acsl_malloc, behavior allocation: postcondition got status unknown, but it is unknown if the behavior is active.
 FRAMAC_SHARE/libc/stdlib.h:132:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid.
-FRAMAC_SHARE/libc/stdlib.h:132:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid, but it is unknown if the behavior is active.
 tests/e-acsl-runtime/valid.c:29:[value] Assertion got status valid.
 ./share/e-acsl/memory_model/e_acsl_mmodel.h:86:[value] Function __initialized: postcondition got status valid.
 tests/e-acsl-runtime/valid.c:29:[kernel] warning: accessing uninitialized left-value: assert \initialized(&b);

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

@@ -40,9 +40,7 @@ tests/e-acsl-runtime/valid.c:27:[value] Non-termination in evaluation of functio
 ./share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
 [value] using specification for function __delete_block
 FRAMAC_SHARE/libc/stdlib.h:127:[value] Function __e_acsl_malloc, behavior allocation: postcondition got status unknown.
-FRAMAC_SHARE/libc/stdlib.h:127:[value] Function __e_acsl_malloc, behavior allocation: postcondition got status unknown, but it is unknown if the behavior is active.
 FRAMAC_SHARE/libc/stdlib.h:132:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid.
-FRAMAC_SHARE/libc/stdlib.h:132:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid, but it is unknown if the behavior is active.
 tests/e-acsl-runtime/valid.c:29:[value] Assertion got status valid.
 ./share/e-acsl/memory_model/e_acsl_mmodel.h:86:[value] Function __initialized: postcondition got status valid.
 tests/e-acsl-runtime/valid.c:29:[kernel] warning: accessing uninitialized left-value: assert \initialized(&b);

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

@@ -38,9 +38,7 @@ tests/e-acsl-runtime/valid_alias.c:12:[value] Non-termination in evaluation of f
 ./share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
 [value] using specification for function __delete_block
 FRAMAC_SHARE/libc/stdlib.h:127:[value] Function __e_acsl_malloc, behavior allocation: postcondition got status unknown.
-FRAMAC_SHARE/libc/stdlib.h:127:[value] Function __e_acsl_malloc, behavior allocation: postcondition got status unknown, but it is unknown if the behavior is active.
 FRAMAC_SHARE/libc/stdlib.h:132:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid.
-FRAMAC_SHARE/libc/stdlib.h:132:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid, but it is unknown if the behavior is active.
 [value] using specification for function __initialize
 tests/e-acsl-runtime/valid_alias.c:16:[value] Assertion got status valid.
 ./share/e-acsl/memory_model/e_acsl_mmodel.h:86:[value] Function __initialized: postcondition got status valid.

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

@@ -38,9 +38,7 @@ tests/e-acsl-runtime/valid_alias.c:12:[value] Non-termination in evaluation of f
 ./share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
 [value] using specification for function __delete_block
 FRAMAC_SHARE/libc/stdlib.h:127:[value] Function __e_acsl_malloc, behavior allocation: postcondition got status unknown.
-FRAMAC_SHARE/libc/stdlib.h:127:[value] Function __e_acsl_malloc, behavior allocation: postcondition got status unknown, but it is unknown if the behavior is active.
 FRAMAC_SHARE/libc/stdlib.h:132:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid.
-FRAMAC_SHARE/libc/stdlib.h:132:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid, but it is unknown if the behavior is active.
 [value] using specification for function __initialize
 tests/e-acsl-runtime/valid_alias.c:16:[value] Assertion got status valid.
 ./share/e-acsl/memory_model/e_acsl_mmodel.h:86:[value] Function __initialized: postcondition got status valid.

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

@@ -24,12 +24,10 @@ tests/e-acsl-runtime/valid_in_contract.c:21:[value] Non-termination in evaluatio
 [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.
 tests/e-acsl-runtime/valid_in_contract.c:22:[value] Function f, behavior B2: postcondition got status valid.
-tests/e-acsl-runtime/valid_in_contract.c:22:[value] Function f, behavior B2: postcondition got status valid, but it is unknown if the behavior is active.
 [value] using specification for function e_acsl_assert
 ./share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
 tests/e-acsl-runtime/valid_in_contract.c:18:[value] Function __e_acsl_f, behavior B1: postcondition got status valid.
 tests/e-acsl-runtime/valid_in_contract.c:22:[value] Function __e_acsl_f, behavior B2: postcondition got status valid.
-tests/e-acsl-runtime/valid_in_contract.c:22:[value] Function __e_acsl_f, behavior B2: postcondition got status valid, but it is unknown if the behavior is active.
 [value] using specification for function __clean
 [kernel] warning: Neither code nor specification for function __clean, generating default assigns from the prototype
 [value] done for function main

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

@@ -24,12 +24,10 @@ tests/e-acsl-runtime/valid_in_contract.c:21:[value] Non-termination in evaluatio
 [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.
 tests/e-acsl-runtime/valid_in_contract.c:22:[value] Function f, behavior B2: postcondition got status valid.
-tests/e-acsl-runtime/valid_in_contract.c:22:[value] Function f, behavior B2: postcondition got status valid, but it is unknown if the behavior is active.
 [value] using specification for function e_acsl_assert
 ./share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
 tests/e-acsl-runtime/valid_in_contract.c:18:[value] Function __e_acsl_f, behavior B1: postcondition got status valid.
 tests/e-acsl-runtime/valid_in_contract.c:22:[value] Function __e_acsl_f, behavior B2: postcondition got status valid.
-tests/e-acsl-runtime/valid_in_contract.c:22:[value] Function __e_acsl_f, behavior B2: postcondition got status valid, but it is unknown if the behavior is active.
 [value] using specification for function __clean
 [kernel] warning: Neither code nor specification for function __clean, generating default assigns from the prototype
 [value] done for function main