From ef3641da21b53e2462845720b24b866f5a833aaf Mon Sep 17 00:00:00 2001
From: Boris Yakobowski <boris.yakobowski@cea.fr>
Date: Tue, 21 Mar 2017 21:57:04 +0100
Subject: [PATCH] Adapt to trunk branch
feature/eva/remove-redundant-alarms-default
---
src/plugins/e-acsl/tests/runtime/oracle/block_valid.res.oracle | 1 +
src/plugins/e-acsl/tests/runtime/oracle/early_exit.res.oracle | 1 +
src/plugins/e-acsl/tests/runtime/oracle/initialized.res.oracle | 1 +
src/plugins/e-acsl/tests/runtime/oracle/mainargs.res.oracle | 1 +
src/plugins/e-acsl/tests/runtime/oracle/memalign.res.oracle | 1 +
src/plugins/e-acsl/tests/runtime/oracle/memsize.res.oracle | 1 +
src/plugins/e-acsl/tests/runtime/oracle/vector.res.oracle | 1 +
7 files changed, 7 insertions(+)
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/block_valid.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/block_valid.res.oracle
index f102d73fa2a..6c86a931f4c 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/block_valid.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/block_valid.res.oracle
@@ -6,3 +6,4 @@ tests/runtime/block_valid.c:45:[value] warning: out of bounds write. assert \val
tests/runtime/block_valid.c:46:[value] warning: out of bounds write. assert \valid(pmax);
tests/runtime/block_valid.c:52:[value] warning: assertion got status unknown.
tests/runtime/block_valid.c:54:[value] warning: assertion got status unknown.
+[scope:rm_asserts] removing 2 assertion(s)
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/early_exit.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/early_exit.res.oracle
index 27ca710aa08..e510a97a7e3 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/early_exit.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/early_exit.res.oracle
@@ -32,3 +32,4 @@ tests/runtime/early_exit.c:117:[value] warning: accessing uninitialized left-val
tests/runtime/early_exit.c:117:[value] warning: accessing left-value that contains escaping addresses.
assert ¬\dangling(&q);
tests/runtime/early_exit.c:99:[value] warning: locals {a0} escaping the scope of a block of while_valid through r
+[scope:rm_asserts] removing 5 assertion(s)
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/initialized.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/initialized.res.oracle
index 442101a5faa..81b19d24dfe 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/initialized.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/initialized.res.oracle
@@ -14,3 +14,4 @@ tests/runtime/initialized.c:94:[value] warning: assertion got status unknown.
tests/runtime/initialized.c:97:[value] warning: assertion got status unknown.
tests/runtime/initialized.c:108:[value] warning: out of bounds write. assert \valid(partsi + i);
tests/runtime/initialized.c:106:[value] warning: out of bounds write. assert \valid(partsc + i);
+[scope:rm_asserts] removing 6 assertion(s)
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/mainargs.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/mainargs.res.oracle
index e3f9a03de82..3204922bbb2 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/mainargs.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/mainargs.res.oracle
@@ -22,3 +22,4 @@ FRAMAC_SHARE/libc/string.h:92:[value] warning: builtin Frama_C_strlen: possibly
FRAMAC_SHARE/libc/string.h:94:[value] warning: function __gen_e_acsl_strlen: postcondition got status unknown.
tests/runtime/mainargs.c:19:[value] warning: assertion got status unknown.
tests/runtime/mainargs.c:20:[value] warning: assertion got status unknown.
+[scope:rm_asserts] removing 1 assertion(s)
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/memalign.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/memalign.res.oracle
index 4ba26f48cd6..a0fd973000e 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/memalign.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/memalign.res.oracle
@@ -3,3 +3,4 @@
tests/runtime/memalign.c:12:[kernel] warning: Neither code nor specification for function posix_memalign, generating default assigns from the prototype
tests/runtime/memalign.c:14:[value] warning: accessing uninitialized left-value. assert \initialized(memptr);
tests/runtime/memalign.c:14:[value] warning: out of bounds read. assert \valid_read(memptr);
+[scope:rm_asserts] removing 2 assertion(s)
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/memsize.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/memsize.res.oracle
index 5f44363c23a..9fcbf305776 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/memsize.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/memsize.res.oracle
@@ -2,3 +2,4 @@
[e-acsl] translation done in project "e-acsl".
tests/runtime/memsize.c:14:[value] warning: assertion got status unknown.
tests/runtime/memsize.c:16:[value] warning: assertion got status invalid (stopping propagation).
+[scope:rm_asserts] removing 6 assertion(s)
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/vector.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/vector.res.oracle
index 38fd6f94cd3..a6402415ce9 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/vector.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/vector.res.oracle
@@ -3,3 +3,4 @@
FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown.
tests/runtime/vector.c:26:[value] warning: accessing uninitialized left-value. assert \initialized(v2 + 2);
tests/runtime/vector.c:28:[value] warning: assertion got status unknown.
+[scope:rm_asserts] removing 1 assertion(s)
--
GitLab