From c9c47b7bebf39582c8039033ebf4879af7c1e88d Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Mon, 22 Oct 2018 17:07:27 +0200
Subject: [PATCH] [tests] use -eva-ignore-recursive-calls where needed
---
src/plugins/e-acsl/tests/bts/bts1395.i | 1 +
.../tests/bts/oracle/bts1395.res.oracle | 22 +++++++++++--------
src/plugins/e-acsl/tests/gmp/longlong.i | 2 +-
.../tests/gmp/oracle/longlong.0.res.oracle | 4 ++--
.../tests/gmp/oracle/longlong.1.res.oracle | 4 ++--
5 files changed, 19 insertions(+), 14 deletions(-)
diff --git a/src/plugins/e-acsl/tests/bts/bts1395.i b/src/plugins/e-acsl/tests/bts/bts1395.i
index a6086e8542a..6b82653a96b 100644
--- a/src/plugins/e-acsl/tests/bts/bts1395.i
+++ b/src/plugins/e-acsl/tests/bts/bts1395.i
@@ -1,5 +1,6 @@
/* run.config
COMMENT: recursive function
+ STDOPT: +"-eva-ignore-recursive-calls"
*/
/*@ requires n > 0; */
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1395.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1395.res.oracle
index 99ac6de8e2a..ea1cf8d1c6a 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1395.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1395.res.oracle
@@ -1,11 +1,15 @@
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
-[eva] tests/bts/bts1395.i:8: Warning:
- detected recursive call
- (__gen_e_acsl_fact <- fact :: tests/bts/bts1395.i:6 <-
- __gen_e_acsl_fact :: tests/bts/bts1395.i:12 <-
- main)
- Use -eva-ignore-recursive-calls to ignore (beware this will make the analysis
- unsound)
-[eva] User Error: Degeneration occurred:
- results are not correct for lines of code that can be reached from the degeneration point.
+[eva] tests/bts/bts1395.i:9: Warning:
+ recursive call during value analysis
+ of __gen_e_acsl_fact (__gen_e_acsl_fact <- fact :: tests/bts/bts1395.i:7 <-
+ __gen_e_acsl_fact :: tests/bts/bts1395.i:13 <-
+ main).
+ Assuming the call has no effect. The analysis will be unsound.
+[eva:alarm] tests/bts/bts1395.i:9: Warning:
+ signed overflow. assert -2147483648 ≤ n * tmp;
+ (tmp from fact(n - 1))
+[eva:alarm] tests/bts/bts1395.i:9: Warning:
+ signed overflow. assert n * tmp ≤ 2147483647;
+ (tmp from fact(n - 1))
+[eva:alarm] tests/bts/bts1395.i:14: Warning: assertion got status unknown.
diff --git a/src/plugins/e-acsl/tests/gmp/longlong.i b/src/plugins/e-acsl/tests/gmp/longlong.i
index bdaa2c9cf17..e013c42e76b 100644
--- a/src/plugins/e-acsl/tests/gmp/longlong.i
+++ b/src/plugins/e-acsl/tests/gmp/longlong.i
@@ -1,6 +1,6 @@
/* run.config
COMMENT: upgrading longlong to GMP
- STDOPT: +"-val-ignore-recursive-calls"
+ STDOPT: +"-eva-ignore-recursive-calls"
*/
unsigned long long my_pow(unsigned int x, unsigned int n) {
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 ad18eafd7c5..5b07e0a1fff 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
@@ -10,10 +10,10 @@
__e_acsl_math_HUGE_VALF ∈ [-3.40282346639e+38 .. 3.40282346639e+38]
__e_acsl_math_INFINITY ∈ [-1.79769313486e+308 .. 1.79769313486e+308]
[eva] using specification for function __e_acsl_memory_init
-[eva] tests/gmp/longlong.i:9: User Error:
+[eva] tests/gmp/longlong.i:9: Warning:
recursive call during value analysis
of my_pow (my_pow <- my_pow :: tests/gmp/longlong.i:16 <- main). Assuming
- the call has no effect. The analysis will be unsound.]
+ the call has no effect. The analysis will be unsound.
[eva] using specification for function my_pow
[eva:alarm] tests/gmp/longlong.i:10: Warning:
signed overflow. assert -2147483648 ≤ tmp * tmp;
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 cf169024abf..fada6aef03d 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
@@ -10,10 +10,10 @@
__e_acsl_math_HUGE_VALF ∈ [-3.40282346639e+38 .. 3.40282346639e+38]
__e_acsl_math_INFINITY ∈ [-1.79769313486e+308 .. 1.79769313486e+308]
[eva] using specification for function __e_acsl_memory_init
-[eva] tests/gmp/longlong.i:9: User Error:
+[eva] tests/gmp/longlong.i:9: Warning:
recursive call during value analysis
of my_pow (my_pow <- my_pow :: tests/gmp/longlong.i:16 <- main). Assuming
- the call has no effect. The analysis will be unsound.]
+ the call has no effect. The analysis will be unsound.
[eva] using specification for function my_pow
[eva:alarm] tests/gmp/longlong.i:10: Warning:
signed overflow. assert -2147483648 ≤ tmp * tmp;
--
GitLab