From bfc615c88219d3c209bbcb4e3cfc504c7605e174 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr> Date: Tue, 19 Jan 2016 14:16:37 +0100 Subject: [PATCH] Update oracles w.r.t. Frama-C trunk (fix the order of the value messages). --- .../tests/e-acsl-runtime/oracle/linear_search.0.res.oracle | 4 ++-- .../tests/e-acsl-runtime/oracle/linear_search.1.res.oracle | 4 ++-- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/linear_search.0.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/linear_search.0.res.oracle index 7b2aac32b7a..a74eb1cb062 100644 --- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/linear_search.0.res.oracle +++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/linear_search.0.res.oracle @@ -24,10 +24,10 @@ tests/e-acsl-runtime/linear_search.i:20:[value] entering loop for the first time 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 valid. (Behavior may be inactive, no reduction performed.) tests/e-acsl-runtime/linear_search.i:12:[value] Function search, behavior exists: postcondition got status invalid. (Behavior may be inactive, no reduction performed.) -tests/e-acsl-runtime/linear_search.i:15:[value] Function search, behavior not_exists: postcondition got status invalid. (Behavior may be inactive, no reduction performed.) +tests/e-acsl-runtime/linear_search.i:12:[value] Function search, behavior exists: postcondition got status valid. (Behavior may be inactive, no reduction performed.) tests/e-acsl-runtime/linear_search.i:15:[value] Function search, behavior not_exists: postcondition got status valid. (Behavior may be inactive, no reduction performed.) +tests/e-acsl-runtime/linear_search.i:15:[value] Function search, behavior not_exists: postcondition got status invalid. (Behavior may be inactive, no reduction performed.) tests/e-acsl-runtime/linear_search.i:12:[value] Function __e_acsl_search, behavior exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.) tests/e-acsl-runtime/linear_search.i:15:[value] Function __e_acsl_search, behavior not_exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.) tests/e-acsl-runtime/linear_search.i:33:[value] Assertion got status unknown. 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 17c82b48988..feccbdb6ddb 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 @@ -47,10 +47,10 @@ 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:20:[kernel] warning: accessing out of bounds index. assert __e_acsl_i_4 < 10; -tests/e-acsl-runtime/linear_search.i:12:[value] Function search, behavior exists: postcondition got status valid. (Behavior may be inactive, no reduction performed.) tests/e-acsl-runtime/linear_search.i:12:[value] Function search, behavior exists: postcondition got status invalid. (Behavior may be inactive, no reduction performed.) -tests/e-acsl-runtime/linear_search.i:15:[value] Function search, behavior not_exists: postcondition got status invalid. (Behavior may be inactive, no reduction performed.) +tests/e-acsl-runtime/linear_search.i:12:[value] Function search, behavior exists: postcondition got status valid. (Behavior may be inactive, no reduction performed.) tests/e-acsl-runtime/linear_search.i:15:[value] Function search, behavior not_exists: postcondition got status valid. (Behavior may be inactive, no reduction performed.) +tests/e-acsl-runtime/linear_search.i:15:[value] Function search, behavior not_exists: postcondition got status invalid. (Behavior may be inactive, no reduction performed.) tests/e-acsl-runtime/linear_search.i:12:[value] Function __e_acsl_search, behavior exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.) tests/e-acsl-runtime/linear_search.i:15:[value] Function __e_acsl_search, behavior not_exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.) tests/e-acsl-runtime/linear_search.i:33:[value] Assertion got status unknown. -- GitLab