diff --git a/src/plugins/value/engine/recursion.ml b/src/plugins/value/engine/recursion.ml index a5abcb4b90ed4470cda6e8ad546d2b8e071ef496..eadcb4cbf943e945f81cd2c325484dbfa62fc092 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 f4e323985bd2d733470e0b542cf2b13ce88e8bcc..b509e3cd30d2a72b002d62dd3b2d65673c12f0c2 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.