diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1324.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1324.1.res.oracle index 356e1b9e003678bb05b4ca64134d1a8ded65905c..825596654322c5fef0db6a6c0ac4e838e75491a6 100644 --- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1324.1.res.oracle +++ b/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 diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1324.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1324.res.oracle index 02eae28e393acbbf8f70b56510ac6365e843bd2c..0b56c08c696d7a25710f46796dadb15880be5502 100644 --- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1324.res.oracle +++ b/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 diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/function_contract.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/function_contract.1.res.oracle index c2bf90b4211d7efc16fc3c789de81e2d25ce2ff4..04bb2885b28b6982239dc8456942754e077adb9c 100644 --- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/function_contract.1.res.oracle +++ b/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. diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/function_contract.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/function_contract.res.oracle index 27d1e2cd1b832a3370978df46d3450ba5d2a73ee..ff25ac1c575c9fa0f397f4c6bd18255c79ace108 100644 --- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/function_contract.res.oracle +++ b/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. diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/linear_search.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/linear_search.1.res.oracle index 6b7fdc015875702a687cb1a5d4f19d0bdc01b88a..bdef4540a6271aa199a845a6d110ca1b0cc3007c 100644 --- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/linear_search.1.res.oracle +++ b/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 diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/linear_search.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/linear_search.res.oracle index ed2ff3fe789c7bf771613960f80dc4b0d916ddc2..dadf840979f440874dc321e5a295f464730cc229 100644 --- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/linear_search.res.oracle +++ b/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 diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/localvar.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/localvar.1.res.oracle index f035ea15556fad1c11375d7c484305072707ab9f..f3fab21a4bb895fa3b7589391dd77749a668a424 100644 --- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/localvar.1.res.oracle +++ b/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. diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/localvar.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/localvar.res.oracle index f035ea15556fad1c11375d7c484305072707ab9f..f3fab21a4bb895fa3b7589391dd77749a668a424 100644 --- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/localvar.res.oracle +++ b/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. diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.1.res.oracle index c45c5580d5bf4c5c2e0591cbe4aa8168fae16235..8630db0db0d1747f3c8d36dbf3bb9e9536423c65 100644 --- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.1.res.oracle +++ b/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); diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.res.oracle index c45c5580d5bf4c5c2e0591cbe4aa8168fae16235..8630db0db0d1747f3c8d36dbf3bb9e9536423c65 100644 --- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.res.oracle +++ 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); diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.1.res.oracle index fab441dda3c325d787ad60179553c46725cd1ae5..14e9f574bb1569d412861dae6040e26278d0f7dc 100644 --- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.1.res.oracle +++ 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. diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.res.oracle index 7df790d6b2d4350bcc1a3051603ae20033a5c11b..d4c0ba7032bdb5e904be034fd0c6a1ccae9d629a 100644 --- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.res.oracle +++ b/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. diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_in_contract.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_in_contract.1.res.oracle index 8c7141f72d68f6ecf372679170669c268a99a517..305aebb2ff266e0d7b7740ec25f9e7ca6e328b43 100644 --- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_in_contract.1.res.oracle +++ b/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 diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_in_contract.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_in_contract.res.oracle index 8c7141f72d68f6ecf372679170669c268a99a517..305aebb2ff266e0d7b7740ec25f9e7ca6e328b43 100644 --- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_in_contract.res.oracle +++ b/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