sig
val save_results : Cil_types.fundec -> bool
val partial_results : unit -> bool
type analysis_target =
[ `Builtin of
string * Builtins.builtin * Eval.cacheable * Cil_types.funspec
| `Def of Cil_types.fundec * bool
| `Spec of Cil_types.funspec ]
val define_analysis_target :
?recursion_depth:int ->
Cil_types.kinstr ->
Cil_types.kernel_function -> Function_calls.analysis_target
val use_spec_instead_of_definition :
?recursion_depth:int -> Cil_types.kernel_function -> bool
val is_called : Cil_types.kernel_function -> bool
val callers : Cil_types.kernel_function -> Cil_types.kernel_function list
val callsites :
Cil_types.kernel_function ->
(Cil_types.kernel_function * Cil_types.stmt list) list
type results = Complete | Partial | NoResults
type analysis_status =
Unreachable
| SpecUsed
| Builtin of string
| Analyzed of Function_calls.results
val analysis_status :
Cil_types.kernel_function -> Function_calls.analysis_status
type t
val get_results : unit -> Function_calls.t
val set_results : Function_calls.t -> unit
val merge_results :
Function_calls.t -> Function_calls.t -> Function_calls.t
end