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.
typeanalysis_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 |
| |
Analyzed of |
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