diff --git a/src/plugins/variadic/tests/defined/oracle/recursive.res.oracle b/src/plugins/variadic/tests/defined/oracle/recursive.res.oracle index 9fcbfae2ed2afb6f4498cd8fc01efebb747ea53f..5324015d6806aa7a23b4631033c9cd693b8cc7d0 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 0757bce330528a5298ebf08e1358a169dcce5d91..35ce1f080d5b5dd8eb702afe9abb829a903d77ec 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)