From d5eff4291e9b64cda54bf15dadbf19bf661ff2b6 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Tue, 3 Nov 2020 11:31:59 +0100
Subject: [PATCH] [variadic] In tests, uses the Eva parameter
-eva-unroll-recursive-calls.
Instead of the deprecated parameter -eva-ignore-recursive-calls.
---
.../variadic/tests/defined/oracle/recursive.res.oracle | 8 ++------
src/plugins/variadic/tests/defined/recursive.i | 2 +-
2 files changed, 3 insertions(+), 7 deletions(-)
diff --git a/src/plugins/variadic/tests/defined/oracle/recursive.res.oracle b/src/plugins/variadic/tests/defined/oracle/recursive.res.oracle
index 9fcbfae2ed2..5324015d680 100644
--- a/src/plugins/variadic/tests/defined/oracle/recursive.res.oracle
+++ b/src/plugins/variadic/tests/defined/oracle/recursive.res.oracle
@@ -6,15 +6,11 @@
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
-[eva] tests/defined/recursive.i:8: Warning:
- recursive call during value analysis
- of f (f <- f :: tests/defined/recursive.i:12 <- main). Assuming the call has
- no effect. The analysis will be unsound.
-[eva] using specification for function f
+[eva] tests/defined/recursive.i:8: detected recursive call of function f.
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function f:
- __retres ∈ [--..--]
+ __retres ∈ {42}
[eva:final-states] Values at end of function main:
/* Generated by Frama-C */
diff --git a/src/plugins/variadic/tests/defined/recursive.i b/src/plugins/variadic/tests/defined/recursive.i
index 0757bce3305..35ce1f080d5 100644
--- a/src/plugins/variadic/tests/defined/recursive.i
+++ b/src/plugins/variadic/tests/defined/recursive.i
@@ -1,5 +1,5 @@
/* run.config
-STDOPT: +"-eva-ignore-recursive-calls"
+STDOPT: +"-eva-unroll-recursive-calls 10"
*/
int f(int a, ...){
if(a <= 0)
--
GitLab