From 1901914f75b73127038c6b434be6d18ee96d4453 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Thu, 9 Jun 2016 15:32:46 +0200
Subject: [PATCH] [tests] update according to Frama-C kernel changes
---
src/plugins/e-acsl/tests/bts/oracle/bts1837.res.oracle | 2 +-
.../tests/e-acsl-runtime/oracle/freeable.res.oracle | 2 +-
.../tests/e-acsl-runtime/oracle/initialized.res.oracle | 8 ++++----
.../e-acsl/tests/e-acsl-runtime/oracle/valid.res.oracle | 4 ++--
.../tests/e-acsl-runtime/oracle/valid_alias.res.oracle | 8 ++++----
.../e-acsl-runtime/oracle/valid_in_contract.res.oracle | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/vector.res.oracle | 2 +-
7 files changed, 14 insertions(+), 14 deletions(-)
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1837.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1837.res.oracle
index 405331f9868..b151b39e10c 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1837.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1837.res.oracle
@@ -1,4 +1,4 @@
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown.
-tests/bts/bts1837.i:18:[value] warning: signed overflow. assert -2147483648 ≤ i-1;
+tests/bts/bts1837.i:18:[kernel] warning: signed overflow. assert -2147483648 ≤ i-1;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/freeable.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/freeable.res.oracle
index bf28a615802..017b046baf3 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/freeable.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/freeable.res.oracle
@@ -22,4 +22,4 @@ FRAMAC_SHARE/libc/stdlib.h:166:[e-acsl] warning: E-ACSL construct `logic functio
Ignoring annotation.
[e-acsl] translation done in project "e-acsl".
tests/e-acsl-runtime/freeable.c:15:[value] warning: assertion got status unknown.
-tests/e-acsl-runtime/freeable.c:15:[value] warning: accessing uninitialized left-value. assert \initialized(&p);
+tests/e-acsl-runtime/freeable.c:15:[kernel] warning: accessing uninitialized left-value. assert \initialized(&p);
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/initialized.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/initialized.res.oracle
index 5be3ab147a5..55ce04ff62d 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/initialized.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/initialized.res.oracle
@@ -57,11 +57,11 @@ tests/e-acsl-runtime/initialized.c:74:[value] warning: assertion got status unkn
tests/e-acsl-runtime/initialized.c:76:[value] warning: assertion got status unknown.
FRAMAC_SHARE/libc/stdlib.h:179:[value] warning: function __gen_e_acsl_free, behavior deallocation: precondition 'freeable' got status unknown. (Behavior may be inactive, no reduction performed.)
FRAMAC_SHARE/libc/stdlib.h:181:[value] warning: function __gen_e_acsl_free, behavior deallocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
-FRAMAC_SHARE/libc/stdlib.h:179:[value] warning: pointer comparison. assert \pointer_comparable(p, (void *)0);
-FRAMAC_SHARE/libc/stdlib.h:178:[value] warning: pointer comparison. assert \pointer_comparable(p, (void *)0);
+FRAMAC_SHARE/libc/stdlib.h:179:[kernel] warning: pointer comparison. assert \pointer_comparable(p, (void *)0);
+FRAMAC_SHARE/libc/stdlib.h:178:[kernel] warning: pointer comparison. assert \pointer_comparable(p, (void *)0);
tests/e-acsl-runtime/initialized.c:84:[value] warning: assertion got status unknown.
tests/e-acsl-runtime/initialized.c:85:[value] warning: assertion got status unknown.
tests/e-acsl-runtime/initialized.c:93:[value] warning: assertion got status unknown.
tests/e-acsl-runtime/initialized.c:96:[value] warning: assertion got status unknown.
-tests/e-acsl-runtime/initialized.c:107:[value] warning: out of bounds write. assert \valid(partsi+i);
-tests/e-acsl-runtime/initialized.c:105:[value] warning: out of bounds write. assert \valid(partsc+i);
+tests/e-acsl-runtime/initialized.c:107:[kernel] warning: out of bounds write. assert \valid(partsi+i);
+tests/e-acsl-runtime/initialized.c:105:[kernel] warning: out of bounds write. assert \valid(partsc+i);
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 e1eb42c942a..1072766860e 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
@@ -26,5 +26,5 @@ FRAMAC_SHARE/libc/stdlib.h:164:[value] warning: function __gen_e_acsl_malloc, be
FRAMAC_SHARE/libc/stdlib.h:169:[value] warning: function __gen_e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
FRAMAC_SHARE/libc/stdlib.h:179:[value] warning: function __gen_e_acsl_free, behavior deallocation: precondition 'freeable' got status unknown.
FRAMAC_SHARE/libc/stdlib.h:181:[value] warning: function __gen_e_acsl_free, behavior deallocation: postcondition got status unknown.
-tests/e-acsl-runtime/valid.c:47:[value] warning: accessing left-value that contains escaping addresses.
- assert ¬\dangling(&a);
+tests/e-acsl-runtime/valid.c:47:[kernel] warning: accessing left-value that contains escaping addresses.
+ assert ¬\dangling(&a);
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 1dc87a8f90d..c2b62019dbd 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
@@ -26,7 +26,7 @@ FRAMAC_SHARE/libc/stdlib.h:169:[value] warning: function __gen_e_acsl_malloc, be
FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown.
FRAMAC_SHARE/libc/stdlib.h:179:[value] warning: function __gen_e_acsl_free, behavior deallocation: precondition 'freeable' got status unknown.
FRAMAC_SHARE/libc/stdlib.h:181:[value] warning: function __gen_e_acsl_free, behavior deallocation: postcondition got status unknown.
-tests/e-acsl-runtime/valid_alias.c:17:[value] warning: accessing left-value that contains escaping addresses.
- assert ¬\dangling(&a);
-tests/e-acsl-runtime/valid_alias.c:17:[value] warning: accessing left-value that contains escaping addresses.
- assert ¬\dangling(&b);
+tests/e-acsl-runtime/valid_alias.c:17:[kernel] warning: accessing left-value that contains escaping addresses.
+ assert ¬\dangling(&a);
+tests/e-acsl-runtime/valid_alias.c:17:[kernel] warning: accessing left-value that contains escaping addresses.
+ assert ¬\dangling(&b);
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 2a5c2bd025e..70d2c3e40bc 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
@@ -1,4 +1,4 @@
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown.
-tests/e-acsl-runtime/valid_in_contract.c:19:[value] warning: out of bounds read. assert \valid_read(&l->next);
+tests/e-acsl-runtime/valid_in_contract.c:19:[kernel] warning: out of bounds read. assert \valid_read(&l->next);
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/vector.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/vector.res.oracle
index 8ea825d52a8..487d30f8fb3 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/vector.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/vector.res.oracle
@@ -26,6 +26,6 @@ FRAMAC_SHARE/libc/stdlib.h:164:[value] warning: function __gen_e_acsl_malloc, be
FRAMAC_SHARE/libc/stdlib.h:169:[value] warning: function __gen_e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
tests/e-acsl-runtime/vector.c:27:[value] warning: assertion got status unknown.
tests/e-acsl-runtime/vector.c:28:[value] warning: assertion got status unknown.
-tests/e-acsl-runtime/vector.c:28:[value] warning: accessing uninitialized left-value. assert \initialized(&LAST);
+tests/e-acsl-runtime/vector.c:28:[kernel] warning: accessing uninitialized left-value. assert \initialized(&LAST);
FRAMAC_SHARE/libc/stdlib.h:179:[value] warning: function __gen_e_acsl_free, behavior deallocation: precondition 'freeable' got status unknown.
FRAMAC_SHARE/libc/stdlib.h:181:[value] warning: function __gen_e_acsl_free, behavior deallocation: postcondition got status unknown.
--
GitLab