From 1e07cc027aa07585f5570e7e1c68ae2725d41539 Mon Sep 17 00:00:00 2001 From: Julien Signoles <julien.signoles@cea.fr> Date: Tue, 18 Dec 2012 08:30:06 +0000 Subject: [PATCH] [E-ACSL] update oracles with few less warnings --- .../tests/e-acsl-runtime/oracle/linear_search.1.res.oracle | 1 - .../e-acsl/tests/e-acsl-runtime/oracle/linear_search.res.oracle | 1 - 2 files changed, 2 deletions(-) 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 3f1404c14e5..8aceb1111a1 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 @@ -7,7 +7,6 @@ tests/e-acsl-runtime/linear_search.i:9:[e-acsl] warning: missing guard for ensuring that the given integer is C-representable tests/e-acsl-runtime/linear_search.i:9:[e-acsl] warning: missing guard for ensuring that the given integer is C-representable tests/e-acsl-runtime/linear_search.i:27:[e-acsl] warning: E-ACSL construct `loop invariant' is not yet supported. Ignoring annotation. -tests/e-acsl-runtime/linear_search.i:27:[e-acsl] warning: E-ACSL construct `loop invariant' is not yet supported. Ignoring annotation. tests/e-acsl-runtime/linear_search.i:11:[e-acsl] warning: missing guard for ensuring that the given integer is C-representable tests/e-acsl-runtime/linear_search.i:14:[e-acsl] warning: missing guard for ensuring that the given integer is C-representable [value] Analyzing a complete application starting at main 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 c133fff64a2..7780e221a63 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 @@ -5,7 +5,6 @@ [kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -IFRAMAC_SHARE/libc ./share/e-acsl/memory_model/e_acsl_bittree.h" [kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -IFRAMAC_SHARE/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h" tests/e-acsl-runtime/linear_search.i:27:[e-acsl] warning: E-ACSL construct `loop invariant' is not yet supported. Ignoring annotation. -tests/e-acsl-runtime/linear_search.i:27:[e-acsl] warning: E-ACSL construct `loop invariant' is not yet supported. Ignoring annotation. [value] Analyzing a complete application starting at main [value] Computing initial state [value] Initial state computed -- GitLab