From b8ac5889a3e78d365dde64905c3ee2f71c54b2dd Mon Sep 17 00:00:00 2001
From: Kostyantyn Vorobyov <kostyantyn.vorobyov@cea.fr>
Date: Thu, 9 Jun 2016 15:53:01 +0200
Subject: [PATCH] Adjust test oracles as per changes in the Frama-C output
---
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/loop.res.oracle | 6 +++---
.../tests/e-acsl-runtime/oracle/mainargs.res.oracle | 10 +++++-----
.../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 +-
.../tests/e-acsl-runtime/oracle/vector.res.oracle | 2 +-
src/plugins/e-acsl/tests/gmp/oracle/arith.0.res.oracle | 2 +-
.../e-acsl/tests/gmp/oracle/longlong.0.res.oracle | 8 ++++----
.../e-acsl/tests/gmp/oracle/longlong.1.res.oracle | 8 ++++----
12 files changed, 31 insertions(+), 31 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 b151b39e10c..405331f9868 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:[kernel] warning: signed overflow. assert -2147483648 ≤ i-1;
+tests/bts/bts1837.i:18:[value] 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 017b046baf3..bf28a615802 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:[kernel] warning: accessing uninitialized left-value. assert \initialized(&p);
+tests/e-acsl-runtime/freeable.c:15:[value] 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 55ce04ff62d..5be3ab147a5 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:[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);
+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);
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:[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);
+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);
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/loop.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/loop.res.oracle
index 7cb422ff4dc..d74ea4ecbeb 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/loop.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/loop.res.oracle
@@ -2,6 +2,6 @@
[e-acsl] translation done in project "e-acsl".
tests/e-acsl-runtime/loop.i:19:[value] warning: loop invariant got status unknown.
FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status invalid.
-tests/e-acsl-runtime/loop.i:19:[kernel] warning: accessing uninitialized left-value.
- assert
- \initialized(&t[(unsigned long)__gen_e_acsl_k_2][(unsigned long)__gen_e_acsl_l_2]);
+tests/e-acsl-runtime/loop.i:19:[value] warning: accessing uninitialized left-value.
+ assert
+ \initialized(&t[(unsigned long)__gen_e_acsl_k_2][(unsigned long)__gen_e_acsl_l_2]);
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/mainargs.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/mainargs.res.oracle
index c6326144037..8f67952b854 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/mainargs.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/mainargs.res.oracle
@@ -13,14 +13,14 @@ FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: preco
tests/e-acsl-runtime/mainargs.c:12:[value] warning: assertion got status unknown.
tests/e-acsl-runtime/mainargs.c:13:[value] warning: assertion got status unknown.
tests/e-acsl-runtime/mainargs.c:15:[value] warning: assertion got status unknown.
-tests/e-acsl-runtime/mainargs.c:15:[kernel] warning: out of bounds read. assert \valid_read(argv+(unsigned long)argc);
+tests/e-acsl-runtime/mainargs.c:15:[value] warning: out of bounds read. assert \valid_read(argv+(unsigned long)argc);
tests/e-acsl-runtime/mainargs.c:16:[value] warning: assertion got status unknown.
-tests/e-acsl-runtime/mainargs.c:16:[kernel] warning: out of bounds read. assert \valid_read(argv+(unsigned long)argc);
+tests/e-acsl-runtime/mainargs.c:16:[value] warning: out of bounds read. assert \valid_read(argv+(unsigned long)argc);
FRAMAC_SHARE/libc/string.h:91:[value] warning: function __gen_e_acsl_strlen: precondition 'valid_string_src' got status unknown.
FRAMAC_SHARE/libc/string.h:91:[value] warning: function strlen: precondition 'valid_string_src' got status unknown.
FRAMAC_SHARE/libc/string.h:93:[value] warning: function __gen_e_acsl_strlen: postcondition got status unknown.
tests/e-acsl-runtime/mainargs.c:19:[value] warning: assertion got status unknown.
tests/e-acsl-runtime/mainargs.c:20:[value] warning: assertion got status unknown.
-tests/e-acsl-runtime/mainargs.c:18:[kernel] warning: out of bounds read. assert \valid_read(argv+i);
-tests/e-acsl-runtime/mainargs.c:19:[kernel] warning: out of bounds read. assert \valid_read(argv+(unsigned long)i);
-tests/e-acsl-runtime/mainargs.c:20:[kernel] warning: out of bounds read. assert \valid_read(argv+(unsigned long)i);
+tests/e-acsl-runtime/mainargs.c:18:[value] warning: out of bounds read. assert \valid_read(argv+i);
+tests/e-acsl-runtime/mainargs.c:19:[value] warning: out of bounds read. assert \valid_read(argv+(unsigned long)i);
+tests/e-acsl-runtime/mainargs.c:20:[value] warning: out of bounds read. assert \valid_read(argv+(unsigned long)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 1072766860e..e1eb42c942a 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:[kernel] warning: accessing left-value that contains escaping addresses.
- assert ¬\dangling(&a);
+tests/e-acsl-runtime/valid.c:47:[value] 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 c2b62019dbd..1dc87a8f90d 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:[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);
+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);
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 70d2c3e40bc..2a5c2bd025e 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:[kernel] warning: out of bounds read. assert \valid_read(&l->next);
+tests/e-acsl-runtime/valid_in_contract.c:19:[value] 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 487d30f8fb3..8ea825d52a8 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:[kernel] warning: accessing uninitialized left-value. assert \initialized(&LAST);
+tests/e-acsl-runtime/vector.c:28:[value] 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.
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/arith.0.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/arith.0.res.oracle
index 0ce34f18808..7b95350061a 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/arith.0.res.oracle
+++ b/src/plugins/e-acsl/tests/gmp/oracle/arith.0.res.oracle
@@ -21,5 +21,5 @@ FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: preco
[value] using specification for function __gmpz_clear
[value] using specification for function __gmpz_init_set_si
[value] using specification for function __gmpz_add
-tests/gmp/arith.i:34:[kernel] warning: signed overflow. assert 1+__gen_e_acsl__7 ≤ 2147483647;
+tests/gmp/arith.i:34:[value] warning: signed overflow. assert 1+__gen_e_acsl__7 ≤ 2147483647;
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/longlong.0.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/longlong.0.res.oracle
index 427396a3100..b22bde80bf3 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/longlong.0.res.oracle
+++ b/src/plugins/e-acsl/tests/gmp/oracle/longlong.0.res.oracle
@@ -16,8 +16,8 @@ tests/gmp/longlong.i:9:[value] warning: recursive call during value analysis
[value] user error: Recursive call on an unspecified function. Using potentially invalid
inferred assigns 'assigns \result \from x, n;'
[value] using specification for function my_pow
-tests/gmp/longlong.i:10:[kernel] warning: signed overflow. assert -2147483648 ≤ tmp*tmp;
-tests/gmp/longlong.i:10:[kernel] warning: signed overflow. assert tmp*tmp ≤ 2147483647;
+tests/gmp/longlong.i:10:[value] warning: signed overflow. assert -2147483648 ≤ tmp*tmp;
+tests/gmp/longlong.i:10:[value] warning: signed overflow. assert tmp*tmp ≤ 2147483647;
[value] using specification for function __gmpz_init_set_ui
[value] using specification for function __gmpz_init
[value] using specification for function __gmpz_import
@@ -29,7 +29,7 @@ FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:88:[value] warning: function __gmpz_import: pre
FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown.
[value] using specification for function __gmpz_tdiv_r
[value] using specification for function __gmpz_get_ui
-tests/gmp/longlong.i:17:[kernel] warning: pointer comparison.
- assert \pointer_comparable((void *)__gen_e_acsl__4, (void *)1);
+tests/gmp/longlong.i:17:[value] warning: pointer comparison.
+ assert \pointer_comparable((void *)__gen_e_acsl__4, (void *)1);
[value] using specification for function __gmpz_clear
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/longlong.1.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/longlong.1.res.oracle
index e24d41cefb7..e216ce90576 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/longlong.1.res.oracle
+++ b/src/plugins/e-acsl/tests/gmp/oracle/longlong.1.res.oracle
@@ -16,8 +16,8 @@ tests/gmp/longlong.i:9:[value] warning: recursive call during value analysis
[value] user error: Recursive call on an unspecified function. Using potentially invalid
inferred assigns 'assigns \result \from x, n;'
[value] using specification for function my_pow
-tests/gmp/longlong.i:10:[kernel] warning: signed overflow. assert -2147483648 ≤ tmp*tmp;
-tests/gmp/longlong.i:10:[kernel] warning: signed overflow. assert tmp*tmp ≤ 2147483647;
+tests/gmp/longlong.i:10:[value] warning: signed overflow. assert -2147483648 ≤ tmp*tmp;
+tests/gmp/longlong.i:10:[value] warning: signed overflow. assert tmp*tmp ≤ 2147483647;
[value] using specification for function __gmpz_init_set_ui
[value] using specification for function __gmpz_init
[value] using specification for function __gmpz_import
@@ -28,7 +28,7 @@ FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:88:[value] warning: function __gmpz_import: pre
[value] using specification for function __e_acsl_assert
FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown.
[value] using specification for function __gmpz_tdiv_r
-tests/gmp/longlong.i:17:[kernel] warning: pointer comparison.
- assert \pointer_comparable((void *)__gen_e_acsl_eq, (void *)0);
+tests/gmp/longlong.i:17:[value] warning: pointer comparison.
+ assert \pointer_comparable((void *)__gen_e_acsl_eq, (void *)0);
[value] using specification for function __gmpz_clear
[value] done for function main
--
GitLab