From 3fcc928e56c8fb001715ec57d7bd7e1d0839e64f Mon Sep 17 00:00:00 2001 From: Julien Signoles <julien.signoles@cea.fr> Date: Thu, 31 Jan 2013 10:27:44 +0000 Subject: [PATCH] [E-ACSL] update oracles according to Value's changes --- .../e-acsl/tests/e-acsl-runtime/oracle/bts1324.1.res.oracle | 2 -- .../e-acsl/tests/e-acsl-runtime/oracle/bts1324.res.oracle | 2 -- .../e-acsl-runtime/oracle/function_contract.1.res.oracle | 4 ++-- .../tests/e-acsl-runtime/oracle/function_contract.res.oracle | 4 ++-- .../tests/e-acsl-runtime/oracle/linear_search.1.res.oracle | 4 ---- .../tests/e-acsl-runtime/oracle/linear_search.res.oracle | 4 ---- .../e-acsl/tests/e-acsl-runtime/oracle/localvar.1.res.oracle | 2 -- .../e-acsl/tests/e-acsl-runtime/oracle/localvar.res.oracle | 2 -- .../e-acsl/tests/e-acsl-runtime/oracle/valid.1.res.oracle | 2 -- .../e-acsl/tests/e-acsl-runtime/oracle/valid.res.oracle | 2 -- .../tests/e-acsl-runtime/oracle/valid_alias.1.res.oracle | 2 -- .../e-acsl/tests/e-acsl-runtime/oracle/valid_alias.res.oracle | 2 -- .../e-acsl-runtime/oracle/valid_in_contract.1.res.oracle | 2 -- .../tests/e-acsl-runtime/oracle/valid_in_contract.res.oracle | 2 -- 14 files changed, 4 insertions(+), 32 deletions(-) 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 356e1b9e003..82559665432 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 02eae28e393..0b56c08c696 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 c2bf90b4211..04bb2885b28 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 27d1e2cd1b8..ff25ac1c575 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 6b7fdc01587..bdef4540a62 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 ed2ff3fe789..dadf840979f 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 f035ea15556..f3fab21a4bb 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 f035ea15556..f3fab21a4bb 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 c45c5580d5b..8630db0db0d 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 c45c5580d5b..8630db0db0d 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 fab441dda3c..14e9f574bb1 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 7df790d6b2d..d4c0ba7032b 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 8c7141f72d6..305aebb2ff2 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 8c7141f72d6..305aebb2ff2 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 -- GitLab