Module Function_calls

module Function_calls: sig .. end

val save_results : Cil_types.fundec -> bool

True if the results should be saved for the given function.

val partial_results : unit -> bool

True if some results are not stored due to options -eva-no-results or -eva-no-results-function.

type analysis_target = [ `Builtin of string * Builtins.builtin * Eval.cacheable * Cil_types.funspec
| `Def of Cil_types.fundec * bool
| `Spec of Cil_types.funspec ]

What is used for the analysis of a given function:

val define_analysis_target : ?recursion_depth:int ->
Cil_types.kinstr ->
Cil_types.kernel_function -> analysis_target

Define the analysis target of a function according to Eva parameters. Also registers the call in tables for the functions below.

val use_spec_instead_of_definition : ?recursion_depth:int -> Cil_types.kernel_function -> bool

Returns true if the Eva analysis use the specification of the given function instead of its body to interpret its calls.

val is_called : Cil_types.kernel_function -> bool

Returns true if the function has been analyzed.

val callers : Cil_types.kernel_function -> Cil_types.kernel_function list

Returns the list of inferred callers of the given function.

val callsites : Cil_types.kernel_function ->
(Cil_types.kernel_function * Cil_types.stmt list) list

Returns the list of inferred callers, and for each of them, the list of callsites (the call statements) inside.

type results = 
| Complete
| Partial
| NoResults
type analysis_status = 
| Unreachable
| SpecUsed
| Builtin of string
| Analyzed of results
val analysis_status : Cil_types.kernel_function -> analysis_status

Returns the current analysis status of a given function.

The functions below are used by Eva_results.ml to save, merge and load the results of multiple Eva analyses.

type t 
val get_results : unit -> t
val set_results : t -> unit
val merge_results : t -> t -> t