From c2ffe8c62eb0ad242ae592332a6f494460004508 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Fri, 5 Mar 2021 15:01:06 +0100
Subject: [PATCH] [Eva] Removes an outdated warning about recursive calls.
---
src/plugins/value/engine/recursion.ml | 25 +++--------------------
tests/value/oracle/recursion.0.res.oracle | 2 --
tests/value/oracle/recursion.1.res.oracle | 2 --
3 files changed, 3 insertions(+), 26 deletions(-)
diff --git a/src/plugins/value/engine/recursion.ml b/src/plugins/value/engine/recursion.ml
index 5fed26af008..ba0ab79f7e2 100644
--- a/src/plugins/value/engine/recursion.ml
+++ b/src/plugins/value/engine/recursion.ml
@@ -25,27 +25,6 @@ open Eval
module Varinfo = Cil_datatype.Varinfo
-(** Recursion *)
-
-(* Our current treatment for recursion -- use the specification for
- the function that begins the recursive cycle -- is incorrect for
- function with formals whose address is taken. Indeed, we do not know
- which "instance" of the formal is updated by the specification. In
- this case, warn the user. *)
-let check_formals_non_referenced kf =
- let formals = Kernel_function.get_formals kf in
- if List.exists (fun vi -> vi.vaddrof) formals then
- Value_parameters.warning ~current:true ~once:true
- "function '%a' (involved in a recursive call) has a formal parameter \
- whose address is taken. Analysis may be unsound."
- Kernel_function.pretty kf
-
-let warn_recursive_call kf =
- Value_parameters.feedback ~once:true ~current:true
- "@[detected recursive call@ of function %a.@]"
- Kernel_function.pretty kf;
- check_formals_non_referenced kf
-
let mark_unknown_requires kinstr kf funspec =
let stmt =
match kinstr with
@@ -174,7 +153,9 @@ let make_stack (kf, depth) =
let get_stack kf depth = VarStack.memo make_stack (kf, depth)
let make_recursion call depth =
- warn_recursive_call call.kf;
+ Value_parameters.feedback ~once:true ~current:true
+ "@[detected recursive call@ of function %a.@]"
+ Kernel_function.pretty call.kf;
let substitution = get_stack call.kf depth in
let add_if_copy acc argument =
match argument.avalue with
diff --git a/tests/value/oracle/recursion.0.res.oracle b/tests/value/oracle/recursion.0.res.oracle
index f069edf3652..fba7f81d0ee 100644
--- a/tests/value/oracle/recursion.0.res.oracle
+++ b/tests/value/oracle/recursion.0.res.oracle
@@ -216,8 +216,6 @@
locals {x} escaping the scope of a block of escaping_local through p
[eva] tests/value/recursion.c:287:
detected recursive call of function escaping_formal.
-[eva] tests/value/recursion.c:287: Warning:
- function 'escaping_formal' (involved in a recursive call) has a formal parameter whose address is taken. Analysis may be unsound.
[eva] tests/value/recursion.c:287: Warning:
Using specification of function escaping_formal for recursive calls.
Analysis of function escaping_formal 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 5d85086961e..03d788a8062 100644
--- a/tests/value/oracle/recursion.1.res.oracle
+++ b/tests/value/oracle/recursion.1.res.oracle
@@ -99,8 +99,6 @@
all target addresses were invalid. This path is assumed to be dead.
[eva] tests/value/recursion.c:287:
detected recursive call of function escaping_formal.
-[eva] tests/value/recursion.c:287: Warning:
- function 'escaping_formal' (involved in a recursive call) has a formal parameter whose address is taken. Analysis may be unsound.
[eva] tests/value/recursion.c:290: Frama_C_show_each_16: {1}
[eva:locals-escaping] tests/value/recursion.c:287: Warning:
locals {x} escaping the scope of escaping_formal through p
--
GitLab