From 963c91a551deaa356abfb30fdcd715fb2ff865b7 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Thu, 29 Apr 2021 16:35:38 +0200
Subject: [PATCH] [Eva] Do not fail on recursive calls without specification.

Instead, emits an error but continues the analysis with the probably unsound
specification generated by the kernel.
Also prints the callstack when -eva-print-callstacks is enabled.
---
 src/plugins/value/engine/recursion.ml     | 15 +++++--
 tests/value/oracle/recursion.2.res.oracle | 49 ++++++++++++++++++++++-
 2 files changed, 58 insertions(+), 6 deletions(-)

diff --git a/src/plugins/value/engine/recursion.ml b/src/plugins/value/engine/recursion.ml
index a5abcb4b90e..eadcb4cbf94 100644
--- a/src/plugins/value/engine/recursion.ml
+++ b/src/plugins/value/engine/recursion.ml
@@ -46,13 +46,20 @@ let mark_unknown_requires kinstr kf funspec =
 
 let get_spec kinstr kf =
   let funspec = Annotations.funspec ~populate:false kf in
-  if Cil.is_empty_funspec funspec then
-    Value_parameters.abort ~current:true
-      "@[Recursive call to %a@ without a specification.@ Try to increase@ \
-       the %s parameter@ or write a specification@ for function %a.@]"
+  if Cil.is_empty_funspec funspec then begin
+    Value_parameters.error ~current:true
+      "@[Recursive call to %a@ without a specification.@ \
+       Generating probably incomplete assigns to interpret the call.@ \
+       Try to increase@ the %s parameter@ \
+       or write a correct specification@ for function %a.%t@]"
       Kernel_function.pretty kf
       Value_parameters.RecursiveUnroll.name
       Kernel_function.pretty kf
+      Value_util.pp_callstack;
+    Cil.CurrentLoc.set (Kernel_function.get_location kf);
+    ignore (!Annotations.populate_spec_ref kf funspec);
+    Annotations.funspec kf
+  end
   else
     let depth = Value_parameters.RecursiveUnroll.get () in
     let () =
diff --git a/tests/value/oracle/recursion.2.res.oracle b/tests/value/oracle/recursion.2.res.oracle
index f4e323985bd..b509e3cd30d 100644
--- a/tests/value/oracle/recursion.2.res.oracle
+++ b/tests/value/oracle/recursion.2.res.oracle
@@ -11,7 +11,52 @@
 [eva] tests/value/recursion.c:437: Frama_C_show_each_36: {36}
 [eva] using specification for function Frama_C_interval
 [eva] tests/value/recursion.c:425: User Error: 
-  Recursive call to sum_nospec without a specification. Try to increase
-  the -eva-unroll-recursive-calls parameter or write a specification
+  Recursive call to sum_nospec without a specification.
+  Generating probably incomplete assigns to interpret the call. Try to increase
+  the -eva-unroll-recursive-calls parameter or write a correct specification
   for function sum_nospec.
+[kernel:annot:missing-spec] tests/value/recursion.c:422: Warning: 
+  Neither code nor specification for function sum_nospec, generating default assigns from the prototype
+[eva] using specification for function sum_nospec
+[eva] tests/value/recursion.c:441: 
+  Frama_C_show_each_unreachable: [-2147483648..2147483647]
+[eva] done for function main_fail
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function sum_nospec:
+  res ∈ [--..--]
+  __retres ∈ [--..--]
+[eva:final-states] Values at end of function main_fail:
+  Frama_C_entropy_source ∈ [--..--]
+  x ∈ [4..16]
+  y ∈ [--..--]
+[from] Computing for function sum_nospec
+[from] Computing for function sum_nospec <-sum_nospec
+[from] Done for function sum_nospec
+[from] Done for function sum_nospec
+[from] Computing for function main_fail
+[from] Computing for function Frama_C_interval <-main_fail
+[from] Done for function Frama_C_interval
+[from] Done for function main_fail
+[from] ====== DEPENDENCIES COMPUTED ======
+  These dependencies hold at termination for the executions that terminate:
+[from] Function Frama_C_interval:
+  Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
+  \result FROM Frama_C_entropy_source; min; max
+[from] Function sum_nospec:
+  res FROM i
+  tmp FROM i
+  __retres FROM i
+  \result FROM i
+[from] Function main_fail:
+  Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
+[from] ====== END OF DEPENDENCIES ======
+[inout] Out (internal) for function sum_nospec:
+    res; tmp; __retres
+[inout] Inputs for function sum_nospec:
+    i; res; tmp; __retres
+[inout] Out (internal) for function main_fail:
+    Frama_C_entropy_source; x; y; tmp; tmp_0; tmp_1
+[inout] Inputs for function main_fail:
+    Frama_C_entropy_source
+[eva] User Error: Deferred error message was emitted during execution. See above messages for more information.
 [kernel] Plug-in eva aborted: invalid user input.
-- 
GitLab