diff --git a/VERSION b/VERSION
index be8e64f5a38cfeb3e1c58884871821fdedcf09c7..e395c9270cf14da055f641dbad906e581e6d33c7 100644
--- a/VERSION
+++ b/VERSION
@@ -1 +1 @@
-25.0
+25.0+dev
diff --git a/opam/opam b/opam/opam
index f3c6d36312c0ebf55fb5654612cd3b8bc3a1d611..815ac9b7932befccdc769f4b6e92cc056416c17a 100644
--- a/opam/opam
+++ b/opam/opam
@@ -1,7 +1,7 @@
opam-version: "2.0"
name: "frama-c"
synopsis: "Platform dedicated to the analysis of source code written in C"
-version: "25.0~beta"
+version: "25.0+dev"
description:"""
Frama-C gathers several analysis techniques in a single collaborative
framework, based on analyzers (called "plug-ins") that can build upon the
@@ -68,7 +68,7 @@ authors: [
homepage: "https://frama-c.com/"
license: "LGPL-2.1-only"
dev-repo: "git+https://git.frama-c.com/pub/frama-c.git"
-doc: "http://frama-c.com/download/user-manual-25.0-beta-Manganese.pdf"
+doc: "http://frama-c.com/download/user-manual-25.0-Manganese.pdf"
bug-reports: "https://git.frama-c.com/pub/frama-c/issues"
tags: [
"deductive"
diff --git a/src/plugins/from/callwise.ml b/src/plugins/from/callwise.ml
index 4891f63d8760583be27bb554abdaccb5c4690a77..f1119b1bed4377aa39a0f9a4b5cc69552238a4de 100644
--- a/src/plugins/from/callwise.ml
+++ b/src/plugins/from/callwise.ml
@@ -64,9 +64,9 @@ let record_callwise_dependencies_in_db call_site froms =
Tbl.replace call_site (Function_Froms.join previous froms)
with Not_found -> Tbl.add call_site froms
-let call_for_individual_froms (call_type, value_initial_state, call_stack) =
+let call_for_individual_froms callstack _kf call_type value_initial_state =
if From_parameters.ForceCallDeps.get () then begin
- let current_function, call_site = List.hd call_stack in
+ let current_function, call_site = List.hd callstack in
let register_from froms =
record_callwise_dependencies_in_db call_site froms;
match !call_froms_stack with
@@ -151,15 +151,13 @@ let compute_call_from_value_states current_function states =
Callwise_Froms.compute_and_return current_function
-let record_for_individual_froms (call_stack, value_res) =
+let record_for_individual_froms callstack cur_kf value_res =
if From_parameters.ForceCallDeps.get () then begin
let froms = match value_res with
- | Value_types.Normal (states, _after_states)
- | Value_types.NormalStore ((states, _after_states), _) ->
- let cur_kf, _ = List.hd call_stack in
+ | Eva.Cvalue_callbacks.Store ({before_stmts}, memexec_counter) ->
let froms =
if Eva.Analysis.save_results cur_kf
- then compute_call_from_value_states cur_kf (Lazy.force states)
+ then compute_call_from_value_states cur_kf (Lazy.force before_stmts)
else Function_Froms.top
in
let pre_state = match !call_froms_stack with
@@ -168,28 +166,21 @@ let record_for_individual_froms (call_stack, value_res) =
in
if From_parameters.VerifyAssigns.get () then
!Db.Value.verify_assigns_froms cur_kf ~pre:pre_state froms;
- (match value_res with
- | Value_types.NormalStore (_, memexec_counter) ->
- MemExec.replace memexec_counter froms
- | _ -> ());
+ MemExec.replace memexec_counter froms;
froms
- | Value_types.Reuse counter ->
+ | Reuse counter ->
MemExec.find counter
in
- end_record call_stack froms
+ end_record callstack froms
end
(* Register our callbacks inside the value analysis *)
-let () = From_parameters.ForceCallDeps.add_update_hook
- (fun _bold bnew ->
- if bnew then begin
- Db.Value.Call_Type_Value_Callbacks.extend_once call_for_individual_froms;
- Db.Value.Record_Value_Callbacks_New.extend_once
- record_for_individual_froms;
- end)
+let () =
+ Eva.Cvalue_callbacks.register_call_hook call_for_individual_froms;
+ Eva.Cvalue_callbacks.register_call_results_hook record_for_individual_froms
let force_compute_all_calldeps ()=
diff --git a/src/plugins/inout/operational_inputs.ml b/src/plugins/inout/operational_inputs.ml
index d0abe639b314d4f961eb13f6b8ca70aa8bb15206..632d4a4bd1a12115325af5944788a0bf50df5447 100644
--- a/src/plugins/inout/operational_inputs.ml
+++ b/src/plugins/inout/operational_inputs.ml
@@ -587,11 +587,10 @@ module Callwise = struct
let call_inout_stack = ref []
- let call_for_callwise_inout (call_type, state, call_stack) =
- let (current_function, ki as call_site) = List.hd call_stack in
+ let call_for_callwise_inout callstack _kf call_type state =
+ let (current_function, ki as call_site) = List.hd callstack in
let merge_inout inout =
- Db.Operational_inputs.Record_Inout_Callbacks.apply
- (call_stack, inout);
+ Db.Operational_inputs.Record_Inout_Callbacks.apply (callstack, inout);
if ki = Kglobal
then merge_call_in_global_tables call_site inout
else
@@ -698,35 +697,30 @@ module Callwise = struct
in
Computer.end_dataflow ()
- let record_for_callwise_inout ((call_stack: Db.Value.callstack), value_res) =
+ let record_for_callwise_inout callstack kf value_res =
let inout = match value_res with
- | Value_types.Normal (states, _after_states)
- | Value_types.NormalStore ((states, _after_states), _) ->
- let kf, _ = List.hd call_stack in
+ | Eva.Cvalue_callbacks.Store ({before_stmts}, memexec_counter) ->
let inout =
if Eva.Analysis.save_results kf
- then compute_call_from_value_states kf call_stack (Lazy.force states)
+ then
+ let cvalue_states = Lazy.force before_stmts in
+ compute_call_from_value_states kf callstack cvalue_states
else top
in
- (match value_res with
- | Value_types.NormalStore (_, memexec_counter) ->
- MemExec.replace memexec_counter inout
- | _ -> ());
+ MemExec.replace memexec_counter inout;
inout
-
- | Value_types.Reuse counter ->
+ | Reuse counter ->
MemExec.find counter
in
- Db.Operational_inputs.Record_Inout_Callbacks.apply
- (call_stack, inout);
- end_record call_stack inout
+ Db.Operational_inputs.Record_Inout_Callbacks.apply (callstack, inout);
+ end_record callstack inout
(* Register our callbacks inside the value analysis *)
let () =
- Db.Value.Record_Value_Callbacks_New.extend_once record_for_callwise_inout;
- Db.Value.Call_Type_Value_Callbacks.extend_once call_for_callwise_inout;;
+ Eva.Cvalue_callbacks.register_call_results_hook record_for_callwise_inout;
+ Eva.Cvalue_callbacks.register_call_hook call_for_callwise_inout
end
diff --git a/src/plugins/value/domains/cvalue/builtins.ml b/src/plugins/value/domains/cvalue/builtins.ml
index e630950b1fd2fbcc3a0dea44b31d44f218c9b301..c5682f2f8573b010bd44f8954b5cf7862387c71c 100644
--- a/src/plugins/value/domains/cvalue/builtins.ml
+++ b/src/plugins/value/domains/cvalue/builtins.ml
@@ -265,14 +265,12 @@ let apply_builtin (builtin:builtin) call ~pre ~post =
let arguments = compute_arguments call.arguments call.rest in
try
let call_result = builtin pre arguments in
- let call_stack = Eva_utils.call_stack () in
let froms =
match call_result with
| Full result -> `Builtin result.c_from
- | States _ -> `Builtin None
- | Result _ -> `Spec (Annotations.funspec call.kf)
+ | States _ | Result _ -> `Builtin None
in
- Db.Value.Call_Type_Value_Callbacks.apply (froms, pre, call_stack);
+ Cvalue_callbacks.apply_call_hooks call.callstack call.kf froms pre;
process_result call post call_result
with
| Invalid_nb_of_args n ->
diff --git a/src/plugins/value/dune b/src/plugins/value/dune
index bbb46ac8f0c97ac0a9b5311d684e52cfb0fff49b..d0285778cc47660df0c498af1f40fde13967ba14 100644
--- a/src/plugins/value/dune
+++ b/src/plugins/value/dune
@@ -65,6 +65,7 @@
builtins_watchpoint
compute_functions
cvalue_backward
+ cvalue_callbacks
cvalue_domain
cvalue_forward
cvalue_init
@@ -165,7 +166,7 @@
(deps
gen-api.sh Eva.ml.in Eva.mli.in
engine/analysis.mli utils/results.mli parameters.mli utils/eva_annotations.mli eval.mli
- domains/cvalue/builtins.mli legacy/eval_terms.mli utils/eva_results.mli utils/unit_tests.mli
+ domains/cvalue/builtins.mli utils/cvalue_callbacks.mli legacy/eval_terms.mli utils/eva_results.mli utils/unit_tests.mli
)
(action (run %{deps}))
)
diff --git a/src/plugins/value/engine/compute_functions.ml b/src/plugins/value/engine/compute_functions.ml
index ac17b268d15e9a6f9819f355b847fbbe84907786..530750b8893c46895e211c3303d70ac4b1a202de 100644
--- a/src/plugins/value/engine/compute_functions.ml
+++ b/src/plugins/value/engine/compute_functions.ml
@@ -184,9 +184,8 @@ module Make (Abstract: Abstractions.Eva) = struct
in
call_result
| Some (states, i) ->
- let stack = Eva_utils.call_stack () in
let cvalue = Abstract.Dom.get_cvalue_or_top init_state in
- Db.Value.Call_Type_Value_Callbacks.apply (`Memexec, cvalue, stack);
+ Cvalue_callbacks.apply_call_hooks call.callstack call.kf `Memexec cvalue;
(* Evaluate the preconditions of kf, to update the statuses
at this call. *)
let spec = Annotations.funspec call.kf in
@@ -202,7 +201,8 @@ module Make (Abstract: Abstractions.Eva) = struct
Self.debug ~dkey
"calling Record_Value_New callbacks on saved previous result";
end;
- Db.Value.Record_Value_Callbacks_New.apply (stack, Value_types.Reuse i);
+ let reuse = Cvalue_callbacks.Reuse i in
+ Cvalue_callbacks.apply_call_results_hooks call.callstack call.kf reuse;
(* call can be cached since it was cached once *)
Transfer.{states; cacheable = Cacheable; builtin=false}
@@ -234,11 +234,10 @@ module Make (Abstract: Abstractions.Eva) = struct
let compute_using_spec_or_body target kinstr call state =
let global = match kinstr with Kglobal -> true | _ -> false in
let pp = not global && Parameters.ValShowProgress.get () in
- let call_stack = Eva_utils.call_stack () in
if pp then
Self.feedback
"@[computing for function %a.@\nCalled from %a.@]"
- Value_types.Callstack.pretty_short call_stack
+ Value_types.Callstack.pretty_short call.callstack
Cil_datatype.Location.pretty (Cil_datatype.Kinstr.loc kinstr);
let cvalue_state = Abstract.Dom.get_cvalue_or_top state in
let compute, kind =
@@ -248,7 +247,7 @@ module Make (Abstract: Abstractions.Eva) = struct
| `Spec funspec ->
compute_using_spec funspec, `Spec funspec
in
- Db.Value.Call_Type_Value_Callbacks.apply (kind, cvalue_state, call_stack);
+ Cvalue_callbacks.apply_call_hooks call.callstack call.kf kind cvalue_state;
let resulting_states, cacheable = compute kinstr call state in
if pp then
Self.feedback
@@ -293,8 +292,8 @@ module Make (Abstract: Abstractions.Eva) = struct
let cvalue_state = Abstract.Dom.get_cvalue_or_top state in
match final_state with
| `Bottom ->
- let cs = Eva_utils.call_stack () in
- Db.Value.Call_Type_Value_Callbacks.apply (`Spec spec, cvalue_state, cs);
+ let kind = `Spec spec in
+ Cvalue_callbacks.apply_call_hooks call.callstack call.kf kind cvalue_state;
let cacheable = Eval.Cacheable in
Transfer.{states; cacheable; builtin=true}
| `Value final_state ->
@@ -352,9 +351,8 @@ module Make (Abstract: Abstractions.Eva) = struct
let compute () =
Eva_utils.push_call_stack kf Kglobal;
store_initial_state kf init_state;
- let call =
- { kf; callstack = []; arguments = []; rest = []; return = None; }
- in
+ let callstack = [kf, Kglobal] in
+ let call = { kf; callstack; arguments = []; rest = []; return = None; } in
let final_result = compute_call Kglobal call None init_state in
let final_states = List.map snd (final_result.Transfer.states) in
let final_state = PowersetDomain.(final_states |> of_list |> join) in
diff --git a/src/plugins/value/engine/iterator.ml b/src/plugins/value/engine/iterator.ml
index 3be91801bcbca06a175e6401925edbe0caf4568e..2fc4a8215b03a066dee2e8499146a89fe38660b4 100644
--- a/src/plugins/value/engine/iterator.ml
+++ b/src/plugins/value/engine/iterator.ml
@@ -448,8 +448,8 @@ module Make_Dataflow
(* TODO: apply on all domains. *)
let states = Partitioning.contents f in
let cvalue_states = gather_cvalues states in
- Db.Value.Compute_Statement_Callbacks.apply
- (stmt, Eva_utils.call_stack (), cvalue_states)
+ let callstack = Eva_utils.call_stack () in
+ Cvalue_callbacks.apply_statement_hooks callstack stmt cvalue_states
let update_vertex ?(widening : bool = false) (v : vertex)
(sources : ('branch * flow) list) : bool =
@@ -723,21 +723,12 @@ module Make_Dataflow
Db.Value.Record_Value_Callbacks.apply
(callstack, merged_pre_cvalues)
end;
- if not (Db.Value.Record_Value_Callbacks_New.is_empty ())
- then begin
- if Parameters.ValShowProgress.get () then
- Self.debug ~dkey:dkey_callbacks
- "now calling Record_Value_New callbacks";
- if Parameters.MemExecAll.get () then
- Db.Value.Record_Value_Callbacks_New.apply
- (callstack,
- Value_types.NormalStore ((merged_pre_cvalues, merged_post_cvalues),
- (Mem_exec.new_counter ())))
- else
- Db.Value.Record_Value_Callbacks_New.apply
- (callstack,
- Value_types.Normal (merged_pre_cvalues, merged_post_cvalues))
- end;
+ let states =
+ Cvalue_callbacks.{ before_stmts = merged_pre_cvalues;
+ after_stmts = merged_post_cvalues }
+ in
+ let results = Cvalue_callbacks.Store (states, Mem_exec.new_counter ()) in
+ Cvalue_callbacks.apply_call_results_hooks callstack kf results;
if not (Db.Value.Record_Value_After_Callbacks.is_empty ())
then begin
if Parameters.ValShowProgress.get () then
diff --git a/src/plugins/value/engine/recursion.ml b/src/plugins/value/engine/recursion.ml
index 9134b02da047024d6cc98b06eceb891721f6108c..fb0da4b9b937d09ce4fa8aac3de912354e5851ab 100644
--- a/src/plugins/value/engine/recursion.ml
+++ b/src/plugins/value/engine/recursion.ml
@@ -179,7 +179,7 @@ let make_recursion call depth =
let make call =
let is_same_kf (f, _) = Kernel_function.equal f call.kf in
let previous_calls = List.filter is_same_kf call.callstack in
- let depth = List.length previous_calls in
+ let depth = List.length previous_calls - 1 in
if depth > 0
then Some (make_recursion call depth)
else None
diff --git a/src/plugins/value/engine/transfer_stmt.ml b/src/plugins/value/engine/transfer_stmt.ml
index 303e69ee16dde632435d82c0f774c42a3d3b122a..09bcb4f40fc720fe7c09bcbe9c2692eb2c10fc34 100644
--- a/src/plugins/value/engine/transfer_stmt.ml
+++ b/src/plugins/value/engine/transfer_stmt.ml
@@ -531,9 +531,9 @@ module Make (Abstract: Abstractions.Eva) = struct
(* ------------------------- Make an Eval.call ---------------------------- *)
(* Create an Eval.call *)
- let create_call kf args =
+ let create_call stmt kf args =
let return = Library_functions.get_retres_vi kf in
- let callstack = Eva_utils.call_stack () in
+ let callstack = (kf, Kstmt stmt) :: Eva_utils.call_stack () in
let arguments, rest =
let formals = Kernel_function.get_formals kf in
let rec format_arguments acc args formals = match args, formals with
@@ -572,12 +572,12 @@ module Make (Abstract: Abstractions.Eva) = struct
let arguments = List.map replace_arg call.arguments in
{ call with arguments; }
- let make_call ~subdivnb kf arguments valuation state =
+ let make_call ~subdivnb stmt kf arguments valuation state =
(* Evaluate the arguments of the call. *)
let determinate = is_determinate kf in
compute_actuals ~subdivnb ~determinate valuation state arguments
>>=: fun (args, valuation) ->
- let call = create_call kf args in
+ let call = create_call stmt kf args in
let recursion = Recursion.make call in
let call = Extlib.opt_fold replace_recursive_call recursion call in
call, recursion, valuation
@@ -731,9 +731,8 @@ module Make (Abstract: Abstractions.Eva) = struct
let cvalue_state = Domain.get_cvalue_or_top state in
Db.Value.Call_Value_Callbacks.apply (cvalue_state, stack_with_call);
Db.Value.merge_initial_state (Eva_utils.call_stack ()) cvalue_state;
- Db.Value.Call_Type_Value_Callbacks.apply
- (`Builtin None, cvalue_state, stack_with_call)
-
+ let kind = `Builtin None in
+ Cvalue_callbacks.apply_call_hooks stack_with_call kf kind cvalue_state
(* --------------------- Process the call statement ---------------------- *)
@@ -756,7 +755,7 @@ module Make (Abstract: Abstractions.Eva) = struct
[(Partition.Key.empty, state)]
else
(* Create the call. *)
- let eval, alarms = make_call ~subdivnb kf args valuation state in
+ let eval, alarms = make_call ~subdivnb stmt kf args valuation state in
Alarmset.emit ki_call alarms;
let states =
let+ call, recursion, valuation = eval in
diff --git a/src/plugins/value/eval.mli b/src/plugins/value/eval.mli
index 76f96cf20bc10c0f141cb2ac03e1448bd620c1b8..c0335e7761b4eb99e365b9775c9ceb7061e78fc5 100644
--- a/src/plugins/value/eval.mli
+++ b/src/plugins/value/eval.mli
@@ -238,7 +238,7 @@ type callstack = call_site list
type ('loc, 'value) call = {
kf: kernel_function; (** The called function. *)
callstack: callstack; (** The current callstack
- (without this call). *)
+ (with this call on top). *)
arguments: ('loc, 'value) argument list; (** The arguments of the call. *)
rest: (exp * ('loc, 'value) assigned) list; (** Extra-arguments. *)
return: varinfo option; (** Fake varinfo to store the
diff --git a/src/plugins/value/utils/cvalue_callbacks.ml b/src/plugins/value/utils/cvalue_callbacks.ml
new file mode 100644
index 0000000000000000000000000000000000000000..9a8be4126b2789f785ffa29ab9434238264a5cfd
--- /dev/null
+++ b/src/plugins/value/utils/cvalue_callbacks.ml
@@ -0,0 +1,84 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2022 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+open Cil_types
+
+let dkey = Self.dkey_callbacks
+
+type callstack = (kernel_function * kinstr) list
+type state = Cvalue.Model.t
+
+type analysis_kind =
+ [ `Builtin of Value_types.call_froms
+ | `Spec of funspec
+ | `Def
+ | `Memexec ]
+
+module Call =
+ Hook.Build
+ (struct type t = callstack * kernel_function * analysis_kind * state end)
+
+let register_call_hook f =
+ Call.extend (fun (callstack, kf, kind, state) -> f callstack kf kind state)
+
+let apply_call_hooks callstack kf kind state =
+ Call.apply (callstack, kf, kind, state);
+ Db.Value.Call_Type_Value_Callbacks.apply (kind, state, callstack)
+
+
+type state_by_stmt = (state Cil_datatype.Stmt.Hashtbl.t) Lazy.t
+type results = { before_stmts: state_by_stmt; after_stmts: state_by_stmt }
+
+type call_results =
+ | Store of results * int
+ | Reuse of int
+
+module Call_Results =
+ Hook.Build (struct type t = callstack * kernel_function * call_results end)
+
+let register_call_results_hook f =
+ Call_Results.extend (fun (callstack, kf, results) -> f callstack kf results)
+
+let apply_call_results_hooks callstack kf call_results =
+ if Parameters.ValShowProgress.get ()
+ && not (Call_Results.is_empty ()
+ && Db.Value.Record_Value_Callbacks_New.is_empty ())
+ then Self.debug ~dkey "now calling Call_Results callbacks";
+ Call_Results.apply (callstack, kf, call_results);
+ let results =
+ match call_results with
+ | Reuse i -> Value_types.Reuse i
+ | Store ({before_stmts; after_stmts}, i) ->
+ Value_types.NormalStore ((before_stmts, after_stmts), i)
+ in
+ Db.Value.Record_Value_Callbacks_New.apply (callstack, results)
+
+
+module Statement =
+ Hook.Build (struct type t = callstack * stmt * state list end)
+
+let register_statement_hook f =
+ Statement.extend (fun (callstack, stmt, states) -> f callstack stmt states)
+
+let apply_statement_hooks callstack stmt states =
+ Statement.apply (callstack, stmt, states);
+ Db.Value.Compute_Statement_Callbacks.apply (stmt, callstack, states)
diff --git a/src/plugins/value/utils/cvalue_callbacks.mli b/src/plugins/value/utils/cvalue_callbacks.mli
new file mode 100644
index 0000000000000000000000000000000000000000..cb26f37aa10beb18fff6f8edc4f9e4eaff19445c
--- /dev/null
+++ b/src/plugins/value/utils/cvalue_callbacks.mli
@@ -0,0 +1,75 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2022 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+[@@@ api_start]
+
+(** Register actions to performed during the Eva analysis,
+ with access to the states of the cvalue domain. *)
+
+type callstack = (Cil_types.kernel_function * Cil_types.kinstr) list
+type state = Cvalue.Model.t
+
+type analysis_kind =
+ [ `Builtin of Value_types.call_froms
+ | `Spec of Cil_types.funspec
+ | `Def
+ | `Memexec ]
+
+(** Registers a function to be applied at the beginning of the analysis of each
+ function call. Arguments of the callback are the callstack of the call,
+ the function called, the kind of analysis performed by Eva for this call,
+ and the cvalue state at the beginning of the call. *)
+val register_call_hook:
+ (callstack -> Cil_types.kernel_function -> analysis_kind -> state -> unit)
+ -> unit
+
+
+type state_by_stmt = (state Cil_datatype.Stmt.Hashtbl.t) Lazy.t
+type results = { before_stmts: state_by_stmt; after_stmts: state_by_stmt }
+
+(** Results of a function call. *)
+type call_results =
+ | Store of results * int
+ (** Cvalue states before and after each statement of the given function,
+ plus a unique integer id for the call. *)
+ | Reuse of int
+ (** The results are the same as a previous call with the given integer id,
+ previously recorded with the [Store] constructor. *)
+
+(** Registers a function to be applied at the end of the analysis of each
+ function call. Arguments of the callback are the callstack of the call,
+ the function called and the cvalue states resulting from its analysis. *)
+val register_call_results_hook:
+ (callstack -> Cil_types.kernel_function -> call_results -> unit)
+ -> unit
+
+[@@@ api_end]
+
+val register_statement_hook:
+ (callstack -> Cil_types.stmt -> state list -> unit) -> unit
+
+val apply_call_hooks:
+ callstack -> Cil_types.kernel_function -> analysis_kind -> state -> unit
+val apply_call_results_hooks:
+ callstack -> Cil_types.kernel_function -> call_results -> unit
+val apply_statement_hooks:
+ callstack -> Cil_types.stmt -> state list -> unit
diff --git a/tests/builtins/oracle/imprecise.res.oracle b/tests/builtins/oracle/imprecise.res.oracle
index c5d23a2cbd6870325adf211e6bde1b09c99cfab4..aac1b7410d2177b68888a0a52de635a1bc3bc49b 100644
--- a/tests/builtins/oracle/imprecise.res.oracle
+++ b/tests/builtins/oracle/imprecise.res.oracle
@@ -228,16 +228,16 @@
[kernel] imprecise.c:114: approximating value to write.
[eva:alarm] imprecise.c:116: Warning: assertion got status unknown.
[eva] Recording results for many_writes
-[kernel] imprecise.c:111:
- more than 200(300) elements to enumerate. Approximating.
-[kernel] imprecise.c:114:
- more than 200(300) elements to enumerate. Approximating.
[from] Computing for function many_writes
[kernel] imprecise.c:111:
more than 200(300) dependencies to update. Approximating.
[kernel] imprecise.c:114:
more than 200(300) dependencies to update. Approximating.
[from] Done for function many_writes
+[kernel] imprecise.c:111:
+ more than 200(300) elements to enumerate. Approximating.
+[kernel] imprecise.c:114:
+ more than 200(300) elements to enumerate. Approximating.
[eva] Done for function many_writes
[eva] computing for function overlap <- main.
Called from imprecise.c:151.
diff --git a/tests/builtins/oracle_equality/imprecise.res.oracle b/tests/builtins/oracle_equality/imprecise.res.oracle
index 1671979a21da9093f750711b69ddf89ae1266418..b06a17f898d8a32e07efd66bfb840b4f06213b94 100644
--- a/tests/builtins/oracle_equality/imprecise.res.oracle
+++ b/tests/builtins/oracle_equality/imprecise.res.oracle
@@ -4,11 +4,11 @@
220a223,224
> [kernel] imprecise.c:111:
> more than 200(300) elements to enumerate. Approximating.
-229,232d232
-< [eva:alarm] imprecise.c:116: Warning: assertion got status unknown.
-< [eva] Recording results for many_writes
+228a233,234
+> [kernel] imprecise.c:114:
+> more than 200(300) elements to enumerate. Approximating.
+237,240d242
< [kernel] imprecise.c:111:
< more than 200(300) elements to enumerate. Approximating.
-234a235,236
-> [eva:alarm] imprecise.c:116: Warning: assertion got status unknown.
-> [eva] Recording results for many_writes
+< [kernel] imprecise.c:114:
+< more than 200(300) elements to enumerate. Approximating.
diff --git a/tests/builtins/oracle_octagon/imprecise.res.oracle b/tests/builtins/oracle_octagon/imprecise.res.oracle
index 86e47c5ed0f3386d84358609df6e197296d4fdb8..9633a07ab0e31c0bef97b7be3027233c2a4bf0db 100644
--- a/tests/builtins/oracle_octagon/imprecise.res.oracle
+++ b/tests/builtins/oracle_octagon/imprecise.res.oracle
@@ -1,11 +1,11 @@
220a221,222
> [kernel] imprecise.c:111:
> more than 200(300) elements to enumerate. Approximating.
-229,232d230
-< [eva:alarm] imprecise.c:116: Warning: assertion got status unknown.
-< [eva] Recording results for many_writes
+228a231,232
+> [kernel] imprecise.c:114:
+> more than 200(300) elements to enumerate. Approximating.
+237,240d240
< [kernel] imprecise.c:111:
< more than 200(300) elements to enumerate. Approximating.
-234a233,234
-> [eva:alarm] imprecise.c:116: Warning: assertion got status unknown.
-> [eva] Recording results for many_writes
+< [kernel] imprecise.c:114:
+< more than 200(300) elements to enumerate. Approximating.
diff --git a/tests/builtins/oracle_symblocs/imprecise.res.oracle b/tests/builtins/oracle_symblocs/imprecise.res.oracle
index 86e47c5ed0f3386d84358609df6e197296d4fdb8..9633a07ab0e31c0bef97b7be3027233c2a4bf0db 100644
--- a/tests/builtins/oracle_symblocs/imprecise.res.oracle
+++ b/tests/builtins/oracle_symblocs/imprecise.res.oracle
@@ -1,11 +1,11 @@
220a221,222
> [kernel] imprecise.c:111:
> more than 200(300) elements to enumerate. Approximating.
-229,232d230
-< [eva:alarm] imprecise.c:116: Warning: assertion got status unknown.
-< [eva] Recording results for many_writes
+228a231,232
+> [kernel] imprecise.c:114:
+> more than 200(300) elements to enumerate. Approximating.
+237,240d240
< [kernel] imprecise.c:111:
< more than 200(300) elements to enumerate. Approximating.
-234a233,234
-> [eva:alarm] imprecise.c:116: Warning: assertion got status unknown.
-> [eva] Recording results for many_writes
+< [kernel] imprecise.c:114:
+< more than 200(300) elements to enumerate. Approximating.
diff --git a/tests/value/oracle/replace_by_show_each.res.oracle b/tests/value/oracle/replace_by_show_each.res.oracle
index 85c7d6b9a717f017cf2449e736a7764c00f81c4d..18b7f724883947d6e3ec4f3e8844af1540c495fc 100644
--- a/tests/value/oracle/replace_by_show_each.res.oracle
+++ b/tests/value/oracle/replace_by_show_each.res.oracle
@@ -6,10 +6,10 @@
x ∈ {0}
[eva] replace_by_show_each.c:23: Frama_C_show_each_2:
[eva] replace_by_show_each.c:25: Frama_C_show_each_1:
-[inout] Warning: no assigns clauses for function Frama_C_show_each_1.
- Results will be imprecise.
[from] Warning: no assigns clauses for function Frama_C_show_each_1.
Results will be imprecise.
+[inout] Warning: no assigns clauses for function Frama_C_show_each_1.
+ Results will be imprecise.
[eva:alarm] replace_by_show_each.c:26: Warning:
signed overflow. assert j + 1 ≤ 2147483647;
[eva] Recording results for main