diff --git a/src/plugins/eva/engine/compute_functions.ml b/src/plugins/eva/engine/compute_functions.ml index dfd18af97e093e6fd1705e05f53e78b4307ae089..c2abf4c3b4aa3490608e31f079b0669f4f207298 100644 --- a/src/plugins/eva/engine/compute_functions.ml +++ b/src/plugins/eva/engine/compute_functions.ml @@ -358,6 +358,8 @@ module Make (Engine: Engine_sig.S) = struct then compute_and_cache_call compute kinstr call state else compute kinstr call state + (* Exported in [Engine_sig.Compute] and used by [Transfer_stmt] when + interpreting a call statement. *) let compute_call stmt = compute_call' (Kstmt stmt) (* ----- Main call -------------------------------------------------------- *) diff --git a/src/plugins/eva/engine/engine_sig.ml b/src/plugins/eva/engine/engine_sig.ml index 8597c629984b8e74733c7ce9fbe152b17ed32ccf..13f1581e360d44f891625363e1a6a67c33df18f3 100644 --- a/src/plugins/eva/engine/engine_sig.ml +++ b/src/plugins/eva/engine/engine_sig.ml @@ -23,40 +23,48 @@ open Cil_types open Eval +(** Results of the analysis of a function call: + - the list of computed abstract states at the return statement of the called + function, associated with their partition key; + - whether the results can safely be stored in the memexec cache. *) type 'state call_result = { states: (Partition.key * 'state) list; cacheable: cacheable; } +(** Analysis of functions, built by the functor [Compute_functions.Make]. *) module type Compute = sig type state type loc type value - (** Compute a call to the main function. *) + (** Analysis of a program from the given main function. Computed states for + each statement are stored in the result tables of each enabled abstract + domain. This is called by [Analysis.compute]. + The initial abstract state is computed according to [lib_entry]: + - if false, non-volatile global variables are initialized according + to their initializers (zero if no explicit initializer). + - if true, non-const global variables are initialized at top. *) val compute_from_entry_point: kernel_function -> lib_entry:bool -> unit - (** Compute a call to the main function from the given initial state. *) + (** Analysis of a program from the given main function and initial state. *) val compute_from_init_state: kernel_function -> state -> unit - (** Compute a call during an analysis *) + (** Analysis of a function call during the Eva analysis. This function is + called by [Transfer_stmt] when interpreting a call statement. + [compute_call stmt call recursion state] analyzes the call [call] at + statement [stmt] in the input abstract state [state]. + If [recursion] is not [None], the call is a recursive call. *) val compute_call: stmt -> (loc, value) call -> recursion option -> state -> state call_result end module type S = sig - (* The four abstractions (values, locations, states and evaluation context). *) - include Abstractions.S - - (* The evaluator for these abstractions *) - module Eval : Evaluation_sig.S - with type state = Dom.t - and type context = Ctx.t - and type value = Val.t - and type loc = Loc.location - and type origin = Dom.origin + (** The four abstractions: values, locations, states and evaluation context, + plus the evaluation engine for these abstractions. *) + include Abstractions.S_with_evaluation module Compute : Compute with type state = Dom.t