From 3919c386e9c2fa905f81dd99947796bb3f665164 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Tue, 20 Apr 2021 11:22:07 +0200
Subject: [PATCH] [Eva] New message key "recursion" for the interpretation of
recursive calls.
---
src/plugins/value/engine/recursion.ml | 3 +-
src/plugins/value/value_parameters.ml | 4 +-
src/plugins/value/value_parameters.mli | 3 +
.../tests/defined/oracle/recursive.res.oracle | 3 +-
tests/value/oracle/recursion.0.res.oracle | 61 +++++++++++-------
tests/value/oracle/recursion.1.res.oracle | 64 +++++++++++--------
tests/value/oracle/recursion.2.res.oracle | 2 +-
7 files changed, 87 insertions(+), 53 deletions(-)
diff --git a/src/plugins/value/engine/recursion.ml b/src/plugins/value/engine/recursion.ml
index f3e7887fe87..634204a9452 100644
--- a/src/plugins/value/engine/recursion.ml
+++ b/src/plugins/value/engine/recursion.ml
@@ -144,7 +144,8 @@ let make_stack (kf, depth) =
let get_stack kf depth = VarStack.memo make_stack (kf, depth)
let make_recursion call depth =
- Value_parameters.feedback ~once:true ~current:true
+ let dkey = Value_parameters.dkey_recursion in
+ Value_parameters.feedback ~dkey ~once:true ~current:true
"@[detected recursive call@ of function %a.@]"
Kernel_function.pretty call.kf;
let substitution = get_stack call.kf depth in
diff --git a/src/plugins/value/value_parameters.ml b/src/plugins/value/value_parameters.ml
index 72d866c18ec..a3d0cb97c50 100644
--- a/src/plugins/value/value_parameters.ml
+++ b/src/plugins/value/value_parameters.ml
@@ -82,11 +82,13 @@ let dkey_incompatible_states = register_category "incompatible-states"
let dkey_iterator = register_category "iterator"
let dkey_callbacks = register_category "callbacks"
let dkey_widening = register_category "widening"
+let dkey_recursion = register_category "recursion"
let () =
let activate dkey = add_debug_keys dkey in
List.iter activate
- [dkey_initial_state; dkey_final_states; dkey_summary; dkey_cvalue_domain]
+ [dkey_initial_state; dkey_final_states; dkey_summary; dkey_cvalue_domain;
+ dkey_recursion; ]
(* Warning categories. *)
let wkey_alarm = register_warn_category "alarm"
diff --git a/src/plugins/value/value_parameters.mli b/src/plugins/value/value_parameters.mli
index aa115396cfb..23ce27ed5de 100644
--- a/src/plugins/value/value_parameters.mli
+++ b/src/plugins/value/value_parameters.mli
@@ -218,6 +218,9 @@ val dkey_callbacks : category
(** Debug category used to print the usage of widenings. *)
val dkey_widening : category
+(** Debug category used to print messages about recursive calls. *)
+val dkey_recursion : category
+
(** Registers available cvalue builtins for the -eva-builtin option. *)
val register_builtin: string -> unit
diff --git a/src/plugins/variadic/tests/defined/oracle/recursive.res.oracle b/src/plugins/variadic/tests/defined/oracle/recursive.res.oracle
index 5324015d680..6b943ccd65a 100644
--- a/src/plugins/variadic/tests/defined/oracle/recursive.res.oracle
+++ b/src/plugins/variadic/tests/defined/oracle/recursive.res.oracle
@@ -6,7 +6,8 @@
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
-[eva] tests/defined/recursive.i:8: detected recursive call of function f.
+[eva:recursion] 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:
diff --git a/tests/value/oracle/recursion.0.res.oracle b/tests/value/oracle/recursion.0.res.oracle
index ac804a41b66..ce21d446188 100644
--- a/tests/value/oracle/recursion.0.res.oracle
+++ b/tests/value/oracle/recursion.0.res.oracle
@@ -5,7 +5,8 @@
[eva:initial-state] Values of globals at initialization
nondet ∈ [--..--]
p ∈ {0}
-[eva] tests/value/recursion.c:18: detected recursive call of function five.
+[eva:recursion] tests/value/recursion.c:18:
+ detected recursive call of function five.
[eva] tests/value/recursion.c:18: Warning:
Using specification of function five for recursive calls.
Analysis of function five is thus incomplete and its soundness
@@ -14,7 +15,8 @@
[eva:alarm] tests/value/recursion.c:15: Warning:
function five: postcondition got status unknown.
[eva] tests/value/recursion.c:342: Frama_C_show_each_5: {5}
-[eva] tests/value/recursion.c:28: detected recursive call of function sum.
+[eva:recursion] tests/value/recursion.c:28:
+ detected recursive call of function sum.
[eva] tests/value/recursion.c:28: Warning:
Using specification of function sum for recursive calls.
Analysis of function sum is thus incomplete and its soundness
@@ -23,33 +25,38 @@
[eva:alarm] tests/value/recursion.c:24: Warning:
function sum: postcondition got status unknown.
[eva] tests/value/recursion.c:344: Frama_C_show_each_91: {91}
-[eva] tests/value/recursion.c:37: detected recursive call of function factorial.
+[eva:recursion] tests/value/recursion.c:37:
+ detected recursive call of function factorial.
[eva] tests/value/recursion.c:37: Warning:
Using specification of function factorial for recursive calls.
Analysis of function factorial is thus incomplete and its soundness
relies on the written specification.
[eva] using specification for function factorial
[eva] tests/value/recursion.c:346: Frama_C_show_each_120: [0..4294967295]
-[eva] tests/value/recursion.c:46: detected recursive call of function syracuse.
+[eva:recursion] tests/value/recursion.c:46:
+ detected recursive call of function syracuse.
[eva] tests/value/recursion.c:46: Warning:
Using specification of function syracuse for recursive calls.
Analysis of function syracuse is thus incomplete and its soundness
relies on the written specification.
[eva] using specification for function syracuse
[eva] tests/value/recursion.c:348: Frama_C_show_each_1: [0..4294967294]
-[eva] tests/value/recursion.c:59: detected recursive call of function fibonacci.
+[eva:recursion] tests/value/recursion.c:59:
+ detected recursive call of function fibonacci.
[eva] tests/value/recursion.c:59: Warning:
Using specification of function fibonacci for recursive calls.
Analysis of function fibonacci is thus incomplete and its soundness
relies on the written specification.
[eva] using specification for function fibonacci
-[eva] tests/value/recursion.c:60: detected recursive call of function fibonacci.
+[eva:recursion] tests/value/recursion.c:60:
+ detected recursive call of function fibonacci.
[eva] tests/value/recursion.c:60: Warning:
Using specification of function fibonacci for recursive calls.
Analysis of function fibonacci is thus incomplete and its soundness
relies on the written specification.
[eva] tests/value/recursion.c:350: Frama_C_show_each_89: [0..4294967295]
-[eva] tests/value/recursion.c:76: detected recursive call of function sum_ptr.
+[eva:recursion] tests/value/recursion.c:76:
+ detected recursive call of function sum_ptr.
[eva] tests/value/recursion.c:76: Warning:
Using specification of function sum_ptr for recursive calls.
Analysis of function sum_ptr is thus incomplete and its soundness
@@ -60,7 +67,7 @@
[eva:alarm] tests/value/recursion.c:69: Warning:
function sum_ptr: postcondition got status unknown.
[eva] tests/value/recursion.c:355: Frama_C_show_each_91: {91}
-[eva] tests/value/recursion.c:89:
+[eva:recursion] tests/value/recursion.c:89:
detected recursive call of function factorial_ptr.
[eva] tests/value/recursion.c:89: Warning:
Using specification of function factorial_ptr for recursive calls.
@@ -70,7 +77,7 @@
[eva:alarm] tests/value/recursion.c:90: Warning:
accessing uninitialized left-value. assert \initialized(&res);
[eva] tests/value/recursion.c:358: Frama_C_show_each_120: [0..4294967295]
-[eva] tests/value/recursion.c:101:
+[eva:recursion] tests/value/recursion.c:101:
detected recursive call of function syracuse_ptr.
[eva] tests/value/recursion.c:101: Warning:
Using specification of function syracuse_ptr for recursive calls.
@@ -80,14 +87,14 @@
[eva:alarm] tests/value/recursion.c:102: Warning:
accessing uninitialized left-value. assert \initialized(&prev_res);
[eva] tests/value/recursion.c:361: Frama_C_show_each_1: [0..4294967294]
-[eva] tests/value/recursion.c:117:
+[eva:recursion] tests/value/recursion.c:117:
detected recursive call of function fibonacci_ptr.
[eva] tests/value/recursion.c:117: Warning:
Using specification of function fibonacci_ptr for recursive calls.
Analysis of function fibonacci_ptr is thus incomplete and its soundness
relies on the written specification.
[eva] using specification for function fibonacci_ptr
-[eva] tests/value/recursion.c:119:
+[eva:recursion] tests/value/recursion.c:119:
detected recursive call of function fibonacci_ptr.
[eva] tests/value/recursion.c:119: Warning:
Using specification of function fibonacci_ptr for recursive calls.
@@ -98,7 +105,7 @@
[eva:alarm] tests/value/recursion.c:120: Warning:
accessing uninitialized left-value. assert \initialized(&y);
[eva] tests/value/recursion.c:364: Frama_C_show_each_89: [0..4294967295]
-[eva] tests/value/recursion.c:137:
+[eva:recursion] tests/value/recursion.c:137:
detected recursive call of function sum_and_fact.
[eva] tests/value/recursion.c:137: Warning:
Using specification of function sum_and_fact for recursive calls.
@@ -111,7 +118,8 @@
function sum_and_fact: postcondition got status unknown.
[eva] tests/value/recursion.c:368:
Frama_C_show_each_36_40320: {36}, [0..4294967288],0%8
-[eva] tests/value/recursion.c:161: detected recursive call of function odd.
+[eva:recursion] tests/value/recursion.c:161:
+ detected recursive call of function odd.
[eva] tests/value/recursion.c:161: Warning:
Using specification of function odd for recursive calls.
Analysis of function odd is thus incomplete and its soundness
@@ -121,7 +129,8 @@
function odd: postcondition got status unknown.
[eva] tests/value/recursion.c:373: Frama_C_show_each_1: {1}, {1}
[eva] tests/value/recursion.c:376: Frama_C_show_each_0: {0}, {0}
-[eva] tests/value/recursion.c:183: detected recursive call of function odd_ptr.
+[eva:recursion] tests/value/recursion.c:183:
+ detected recursive call of function odd_ptr.
[eva] tests/value/recursion.c:183: Warning:
Using specification of function odd_ptr for recursive calls.
Analysis of function odd_ptr is thus incomplete and its soundness
@@ -133,7 +142,8 @@
accessing uninitialized left-value. assert \initialized(&y);
[eva:alarm] tests/value/recursion.c:179: Warning:
function even_ptr: postcondition got status unknown.
-[eva] tests/value/recursion.c:171: detected recursive call of function even_ptr.
+[eva:recursion] tests/value/recursion.c:171:
+ detected recursive call of function even_ptr.
[eva] tests/value/recursion.c:379: Frama_C_show_each_1: {1}, {1}
[eva] tests/value/recursion.c:382: Frama_C_show_each_0: {0}, {0}
[eva] using specification for function Frama_C_interval
@@ -145,7 +155,7 @@
function fill_array: precondition got status invalid.
[eva:alarm] tests/value/recursion.c:226: Warning:
function fill_array: precondition got status unknown.
-[eva] tests/value/recursion.c:200:
+[eva:recursion] tests/value/recursion.c:200:
detected recursive call of function fill_array.
[eva] tests/value/recursion.c:200: Warning:
Using specification of function fill_array for recursive calls.
@@ -158,14 +168,14 @@
function fill_array: postcondition got status unknown.
[eva:alarm] tests/value/recursion.c:228: Warning:
function binary_search: precondition \initialized(data + (start .. end)) got status unknown.
-[eva] tests/value/recursion.c:214:
+[eva:recursion] tests/value/recursion.c:214:
detected recursive call of function binary_search.
[eva] tests/value/recursion.c:214: Warning:
Using specification of function binary_search for recursive calls.
Analysis of function binary_search is thus incomplete and its soundness
relies on the written specification.
[eva] using specification for function binary_search
-[eva] tests/value/recursion.c:216:
+[eva:recursion] tests/value/recursion.c:216:
detected recursive call of function binary_search.
[eva] tests/value/recursion.c:216: Warning:
Using specification of function binary_search for recursive calls.
@@ -181,7 +191,8 @@
Frama_C_show_each_7_11: [-2147483648..2147483647]
[eva] tests/value/recursion.c:241:
Frama_C_show_each_minus_1_15: [-2147483648..2147483647]
-[eva] tests/value/recursion.c:252: detected recursive call of function alarm.
+[eva:recursion] tests/value/recursion.c:252:
+ detected recursive call of function alarm.
[eva] tests/value/recursion.c:252: Warning:
Using specification of function alarm for recursive calls.
Analysis of function alarm is thus incomplete and its soundness
@@ -194,7 +205,8 @@
(tmp from alarm(i - 1))
[eva] tests/value/recursion.c:406:
Frama_C_show_each_unreachable: [20..2147483640],0%20
-[eva] tests/value/recursion.c:261: detected recursive call of function precond.
+[eva:recursion] tests/value/recursion.c:261:
+ detected recursive call of function precond.
[eva] tests/value/recursion.c:261: Warning:
Using specification of function precond for recursive calls.
Analysis of function precond is thus incomplete and its soundness
@@ -204,7 +216,7 @@
[eva] using specification for function precond
[eva] tests/value/recursion.c:261: Warning:
Cannot handle empty assigns clause. Assuming assigns \nothing: be aware this is probably incorrect.
-[eva] tests/value/recursion.c:276:
+[eva:recursion] tests/value/recursion.c:276:
detected recursive call of function escaping_local.
[eva] tests/value/recursion.c:276: Warning:
Using specification of function escaping_local for recursive calls.
@@ -216,7 +228,7 @@
[eva] tests/value/recursion.c:279: Frama_C_show_each_1: {5}
[eva:locals-escaping] tests/value/recursion.c:277: Warning:
locals {x} escaping the scope of a block of escaping_local through p
-[eva] tests/value/recursion.c:291:
+[eva:recursion] tests/value/recursion.c:291:
detected recursive call of function escaping_formal.
[eva] tests/value/recursion.c:291: Warning:
Using specification of function escaping_formal for recursive calls.
@@ -228,7 +240,7 @@
[eva] tests/value/recursion.c:294: Frama_C_show_each_1: {5}
[eva:locals-escaping] tests/value/recursion.c:411: Warning:
locals {x} escaping the scope of escaping_formal through p
-[eva] tests/value/recursion.c:307:
+[eva:recursion] tests/value/recursion.c:307:
detected recursive call of function escaping_stack.
[eva] tests/value/recursion.c:307: Warning:
Using specification of function escaping_stack for recursive calls.
@@ -240,7 +252,8 @@
[eva] tests/value/recursion.c:310: Frama_C_show_each_1_2: {5}
[eva:locals-escaping] tests/value/recursion.c:308: Warning:
locals {x} escaping the scope of a block of escaping_stack through p
-[eva] tests/value/recursion.c:323: detected recursive call of function decr.
+[eva:recursion] tests/value/recursion.c:323:
+ detected recursive call of function decr.
[eva] tests/value/recursion.c:323: Warning:
Using specification of function decr for recursive calls.
Analysis of function decr is thus incomplete and its soundness
diff --git a/tests/value/oracle/recursion.1.res.oracle b/tests/value/oracle/recursion.1.res.oracle
index 345219cb76f..5fd6d46ceb1 100644
--- a/tests/value/oracle/recursion.1.res.oracle
+++ b/tests/value/oracle/recursion.1.res.oracle
@@ -5,7 +5,8 @@
[eva:initial-state] Values of globals at initialization
nondet ∈ [--..--]
p ∈ {0}
-[eva] tests/value/recursion.c:18: detected recursive call of function five.
+[eva:recursion] tests/value/recursion.c:18:
+ detected recursive call of function five.
[eva] tests/value/recursion.c:18: Warning:
Using specification of function five for recursive calls of depth 20.
Analysis of function five is thus incomplete and its soundness
@@ -14,37 +15,47 @@
[eva:alarm] tests/value/recursion.c:15: Warning:
function five: postcondition got status unknown.
[eva] tests/value/recursion.c:342: Frama_C_show_each_5: {5}
-[eva] tests/value/recursion.c:28: detected recursive call of function sum.
+[eva:recursion] tests/value/recursion.c:28:
+ detected recursive call of function sum.
[eva] tests/value/recursion.c:344: Frama_C_show_each_91: {91}
-[eva] tests/value/recursion.c:37: detected recursive call of function factorial.
+[eva:recursion] tests/value/recursion.c:37:
+ detected recursive call of function factorial.
[eva] tests/value/recursion.c:346: Frama_C_show_each_120: {120}
-[eva] tests/value/recursion.c:46: detected recursive call of function syracuse.
+[eva:recursion] tests/value/recursion.c:46:
+ detected recursive call of function syracuse.
[eva] tests/value/recursion.c:348: Frama_C_show_each_1: {1}
-[eva] tests/value/recursion.c:59: detected recursive call of function fibonacci.
-[eva] tests/value/recursion.c:60: detected recursive call of function fibonacci.
+[eva:recursion] tests/value/recursion.c:59:
+ detected recursive call of function fibonacci.
+[eva:recursion] tests/value/recursion.c:60:
+ detected recursive call of function fibonacci.
[eva] tests/value/recursion.c:350: Frama_C_show_each_89: {89}
-[eva] tests/value/recursion.c:76: detected recursive call of function sum_ptr.
+[eva:recursion] tests/value/recursion.c:76:
+ detected recursive call of function sum_ptr.
[eva] tests/value/recursion.c:355: Frama_C_show_each_91: {91}
-[eva] tests/value/recursion.c:89:
+[eva:recursion] tests/value/recursion.c:89:
detected recursive call of function factorial_ptr.
[eva] tests/value/recursion.c:358: Frama_C_show_each_120: {120}
-[eva] tests/value/recursion.c:101:
+[eva:recursion] tests/value/recursion.c:101:
detected recursive call of function syracuse_ptr.
[eva] tests/value/recursion.c:361: Frama_C_show_each_1: {1}
-[eva] tests/value/recursion.c:117:
+[eva:recursion] tests/value/recursion.c:117:
detected recursive call of function fibonacci_ptr.
-[eva] tests/value/recursion.c:119:
+[eva:recursion] tests/value/recursion.c:119:
detected recursive call of function fibonacci_ptr.
[eva] tests/value/recursion.c:364: Frama_C_show_each_89: {89}
-[eva] tests/value/recursion.c:137:
+[eva:recursion] tests/value/recursion.c:137:
detected recursive call of function sum_and_fact.
[eva] tests/value/recursion.c:368: Frama_C_show_each_36_40320: {36}, {40320}
-[eva] tests/value/recursion.c:161: detected recursive call of function odd.
-[eva] tests/value/recursion.c:152: detected recursive call of function even.
+[eva:recursion] tests/value/recursion.c:161:
+ detected recursive call of function odd.
+[eva:recursion] tests/value/recursion.c:152:
+ detected recursive call of function even.
[eva] tests/value/recursion.c:373: Frama_C_show_each_1: {1}, {1}
[eva] tests/value/recursion.c:376: Frama_C_show_each_0: {0}, {0}
-[eva] tests/value/recursion.c:183: detected recursive call of function odd_ptr.
-[eva] tests/value/recursion.c:171: detected recursive call of function even_ptr.
+[eva:recursion] tests/value/recursion.c:183:
+ detected recursive call of function odd_ptr.
+[eva:recursion] tests/value/recursion.c:171:
+ detected recursive call of function even_ptr.
[eva] tests/value/recursion.c:379: Frama_C_show_each_1: {1}, {1}
[eva] tests/value/recursion.c:382: Frama_C_show_each_0: {0}, {0}
[eva] using specification for function Frama_C_interval
@@ -60,7 +71,7 @@
function fill_array: precondition got status invalid.
[eva:alarm] tests/value/recursion.c:226: Warning:
function fill_array: precondition got status unknown.
-[eva] tests/value/recursion.c:200:
+[eva:recursion] tests/value/recursion.c:200:
detected recursive call of function fill_array.
[eva:alarm] tests/value/recursion.c:200: Warning:
function fill_array: precondition got status unknown.
@@ -72,23 +83,25 @@
function fill_array: postcondition got status unknown.
[eva:alarm] tests/value/recursion.c:228: Warning:
function binary_search: precondition \initialized(data + (start .. end)) got status unknown.
-[eva] tests/value/recursion.c:214:
+[eva:recursion] tests/value/recursion.c:214:
detected recursive call of function binary_search.
[eva] tests/value/recursion.c:229: Frama_C_show_each_3: {3}
-[eva] tests/value/recursion.c:216:
+[eva:recursion] tests/value/recursion.c:216:
detected recursive call of function binary_search.
[eva] tests/value/recursion.c:231: Frama_C_show_each_12: {12}
[eva] tests/value/recursion.c:233: Frama_C_show_each_minus1: {-1}
[eva] tests/value/recursion.c:238: Frama_C_show_each_7_11: {7; 8; 9; 10; 11}
[eva] tests/value/recursion.c:241: Frama_C_show_each_minus_1_15: [-1..15]
-[eva] tests/value/recursion.c:252: detected recursive call of function alarm.
+[eva:recursion] tests/value/recursion.c:252:
+ detected recursive call of function alarm.
[eva:alarm] tests/value/recursion.c:252: Warning:
signed overflow. assert i * tmp ≤ 2147483647;
(tmp from alarm(i - 1))
-[eva] tests/value/recursion.c:261: detected recursive call of function precond.
+[eva:recursion] tests/value/recursion.c:261:
+ detected recursive call of function precond.
[eva:alarm] tests/value/recursion.c:261: Warning:
function precond: precondition got status invalid.
-[eva] tests/value/recursion.c:276:
+[eva:recursion] tests/value/recursion.c:276:
detected recursive call of function escaping_local.
[eva] tests/value/recursion.c:279: Frama_C_show_each_1: {1}
[eva:locals-escaping] tests/value/recursion.c:277: Warning:
@@ -98,7 +111,7 @@
assert ¬\dangling(&p);
[kernel] tests/value/recursion.c:278: Warning:
all target addresses were invalid. This path is assumed to be dead.
-[eva] tests/value/recursion.c:291:
+[eva:recursion] tests/value/recursion.c:291:
detected recursive call of function escaping_formal.
[eva] tests/value/recursion.c:294: Frama_C_show_each_1: {1}
[eva:locals-escaping] tests/value/recursion.c:291: Warning:
@@ -108,7 +121,7 @@
assert ¬\dangling(&p);
[kernel] tests/value/recursion.c:293: Warning:
all target addresses were invalid. This path is assumed to be dead.
-[eva] tests/value/recursion.c:307:
+[eva:recursion] tests/value/recursion.c:307:
detected recursive call of function escaping_stack.
[eva] tests/value/recursion.c:310: Frama_C_show_each_1_2: {1}
[eva] tests/value/recursion.c:310: Frama_C_show_each_1_2: {2}
@@ -119,7 +132,8 @@
assert ¬\dangling(&p);
[kernel] tests/value/recursion.c:309: Warning:
all target addresses were invalid. This path is assumed to be dead.
-[eva] tests/value/recursion.c:323: detected recursive call of function decr.
+[eva:recursion] tests/value/recursion.c:323:
+ detected recursive call of function decr.
[eva] tests/value/recursion.c:323: Warning:
Using specification of function decr for recursive calls of depth 20.
Analysis of function decr is thus incomplete and its soundness
diff --git a/tests/value/oracle/recursion.2.res.oracle b/tests/value/oracle/recursion.2.res.oracle
index fec49fb9c00..c4c6916fda1 100644
--- a/tests/value/oracle/recursion.2.res.oracle
+++ b/tests/value/oracle/recursion.2.res.oracle
@@ -5,7 +5,7 @@
[eva:initial-state] Values of globals at initialization
nondet ∈ [--..--]
p ∈ {0}
-[eva] tests/value/recursion.c:422:
+[eva:recursion] tests/value/recursion.c:422:
detected recursive call of function sum_nospec.
[eva] tests/value/recursion.c:429: Frama_C_show_each_10: {10}
[eva] tests/value/recursion.c:434: Frama_C_show_each_36: {36}
--
GitLab