[Eva] Removes an outdated warning about recursive calls.

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

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

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