From f6d069d40d69583103aae1a2d937435e0e229bea Mon Sep 17 00:00:00 2001
From: Boris Yakobowski <boris.yakobowski@cea.fr>
Date: Mon, 13 Nov 2017 11:12:23 +0100
Subject: [PATCH] Fix test currently broken
(See frama-c/e-acsl!169)
---
src/plugins/e-acsl/tests/gmp/cast.i | 2 +-
src/plugins/e-acsl/tests/gmp/oracle/cast.0.res.oracle | 2 --
src/plugins/e-acsl/tests/gmp/oracle/cast.1.res.oracle | 2 --
3 files changed, 1 insertion(+), 5 deletions(-)
diff --git a/src/plugins/e-acsl/tests/gmp/cast.i b/src/plugins/e-acsl/tests/gmp/cast.i
index 700d338841e..3b014c861ad 100644
--- a/src/plugins/e-acsl/tests/gmp/cast.i
+++ b/src/plugins/e-acsl/tests/gmp/cast.i
@@ -20,7 +20,7 @@ int main(void) {
/* heterogeneous casts from/to integers */
int t[2] = { 0, 1 };
- /*@ assert (float)x == t[(int)0.1]; */
+ /*@ assert (float)x == (float)t[(int)0.1]; */
return 0;
}
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/cast.0.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/cast.0.res.oracle
index 560ddd4e17b..c7d593ec80c 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/cast.0.res.oracle
+++ b/src/plugins/e-acsl/tests/gmp/oracle/cast.0.res.oracle
@@ -16,6 +16,4 @@ tests/gmp/cast.i:23:[e-acsl] warning: approximating a real number by a float
__e_acsl_math_INFINITY ∈ [-1.79769313486e+308 .. 1.79769313486e+308]
[value] using specification for function __e_acsl_memory_init
[value] using specification for function __e_acsl_assert
-[value] user error: type long double wider than 64 bits not supported.
- Using double instead for the remainder of the analysis.
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/cast.1.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/cast.1.res.oracle
index 23514bf035f..d4f8dd847ac 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/cast.1.res.oracle
+++ b/src/plugins/e-acsl/tests/gmp/oracle/cast.1.res.oracle
@@ -23,8 +23,6 @@ FRAMAC_SHARE/e-acsl/e_acsl.h:94:[value] warning: function __e_acsl_assert: preco
[value] using specification for function __gmpz_clear
[value] using specification for function __gmpz_get_ui
[value] using specification for function __gmpz_init_set_ui
-[value] user error: type long double wider than 64 bits not supported.
- Using double instead for the remainder of the analysis.
tests/gmp/cast.i:23:[value] warning: accessing out of bounds index. assert 0 ≤ __gen_e_acsl_cast_9;
tests/gmp/cast.i:23:[value] warning: accessing out of bounds index. assert __gen_e_acsl_cast_9 < 2;
[value] done for function main
--
GitLab