Skip to content
Snippets Groups Projects
Commit d5eff429 authored by David Bühler's avatar David Bühler
Browse files

[variadic] In tests, uses the Eva parameter -eva-unroll-recursive-calls.

Instead of the deprecated parameter -eva-ignore-recursive-calls.
parent fb6421ec
No related branches found
No related tags found
No related merge requests found
...@@ -6,15 +6,11 @@ ...@@ -6,15 +6,11 @@
[eva] Analyzing a complete application starting at main [eva] Analyzing a complete application starting at main
[eva] Computing initial state [eva] Computing initial state
[eva] Initial state computed [eva] Initial state computed
[eva] tests/defined/recursive.i:8: Warning: [eva] tests/defined/recursive.i:8: detected recursive call of function f.
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] done for function main [eva] done for function main
[eva] ====== VALUES COMPUTED ====== [eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function f: [eva:final-states] Values at end of function f:
__retres ∈ [--..--] __retres ∈ {42}
[eva:final-states] Values at end of function main: [eva:final-states] Values at end of function main:
/* Generated by Frama-C */ /* Generated by Frama-C */
......
/* run.config /* run.config
STDOPT: +"-eva-ignore-recursive-calls" STDOPT: +"-eva-unroll-recursive-calls 10"
*/ */
int f(int a, ...){ int f(int a, ...){
if(a <= 0) if(a <= 0)
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment