Frama-C:
Plug-ins:
Libraries:

Frama-C API - Function_calls

val save_results : Frama_c_kernel.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 = [
  1. | `Builtin of string * Builtins.builtin * Eval.cacheable * Frama_c_kernel.Cil_types.funspec
  2. | `Spec of Frama_c_kernel.Cil_types.funspec
  3. | `Body of Frama_c_kernel.Cil_types.fundec * bool
]

What is used for the analysis of a given function:

  • a Cvalue builtin (and other domains use the specification)
  • the function specification
  • the function body. The boolean indicates whether the resulting states must be recorded at each statement of this function.

Returns the analysis target of a given function at a given callsite according to Eva parameters.

val use_spec_instead_of_definition : ?recursion_depth:int -> Frama_c_kernel.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 register_analysis_target : ('l, 'v) Eval.call -> analysis_target -> unit

Registers the analysis of a call with a given target for functions below.

Returns true if the function has been analyzed.

Returns the list of inferred callers of the given function.

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

val nb_callsites : unit -> int

Returns the number of callsites that have been analyzed.

type results =
  1. | Complete
  2. | Partial
  3. | NoResults
type analysis_status =
  1. | Unreachable
  2. | SpecUsed
  3. | Builtin of string
  4. | Analyzed of results

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