Frama-C API - `Results`

Eva's result API is a new interface to access the results of an analysis, once it is completed. It may slightly change in the future.

The idea behind this API is that requests must be decomposed in several steps. For instance, to evaluate an expression :

1. first, you have to state where you want to evaluate it, 2. optionally, you may specify in which callstack, 3. you choose the expression to evaluate, 4. you require a destination type to evaluate into.

Usage sketch :

Eva.Results.( before stmt |> in_callstack cs |> eval_var vi |> as_int |> default 0)

or equivalently, if you prefer

Eva.Results.( default O (as_int (eval_var vi (in_callstack cs (before stmt))))

val are_available : Frama_c_kernel.Cil_types.kernel_function -> bool

Are results available for a given function? True if the function body has been has been analyzed and the results have been saved. False if:

the function has not been reached by the analysis: all requests in the function will lead to a Bottom error.
a specification or a builtin has been used instead of analyzing the function body: all requests in the function will lead to a Bottom error.
results have not been saved, due to the -eva-no-results parameter: all requests in the function will lead to a Top error.

type request

type value

type address

type 'a evaluation

type error =

| Bottom
| Top
| DisabledDomain

type 'a result = ('a, error) Frama_c_kernel.Result.t

Results handling

val string_of_error : error -> string

Translates an error to a human readable string.

val pretty_error : Stdlib.Format.formatter -> error -> unit

Pretty printer for errors.

val pretty_result : (Stdlib.Format.formatter -> 'a -> unit) -> Stdlib.Format.formatter -> 'a result -> unit

Pretty printer for API's results.

val default : 'a -> 'a result -> 'a

default d r extracts the value of r if r is Ok, or use the default value d otherwise. Equivalent to Result.value ~default:d r

Control point selection

val at_start : request

At the start of the analysis, but after the initialization of globals.

val at_end : unit -> request

At the end of the analysis, after the main function has returned.

val at_start_of : Frama_c_kernel.Cil_types.kernel_function -> request

At the start of the given function.

val at_end_of : Frama_c_kernel.Cil_types.kernel_function -> request

At the end of the given function.

raises Kernel_function.No_statement
if the function has no body.

val before : Frama_c_kernel.Cil_types.stmt -> request

Just before a statement is executed.

val after : Frama_c_kernel.Cil_types.stmt -> request

Just after a statement is executed.

val before_kinstr : Frama_c_kernel.Cil_types.kinstr -> request

Just before a statement or at the start of the analysis.

val in_cvalue_state : Frama_c_kernel.Cvalue.Model.t -> request

Evaluation in a given cvalue state. Callstacks selection are silently ignored on such requests. For internal use, could be modified or removed in a future version.

Callstack selection

val in_callstack : Callstack.t -> request -> request

Only consider the given callstack. Replaces previous calls to in_callstack or in_callstacks.

val in_callstacks : Callstack.t list -> request -> request

Only consider the callstacks from the given list. Replaces previous calls to in_callstack or in_callstacks.

val filter_callstack : (Callstack.t -> bool) -> request -> request

Only consider callstacks satisfying the given predicate. Several filters can be added. If callstacks are also selected with in_callstack or in_callstacks, only the selected callstacks will be filtered.

Working with callstacks

val callstacks : request -> Callstack.t list

Returns the list of reachable callstacks from the given request. An empty list is returned if the request control point has not been reached by the analysis, or if no information has been saved at this point (for instance with the -eva-no-results option). Use is_empty request to distinguish these two cases.

val by_callstack : request -> (Callstack.t * request) list

Returns a list of subrequests for each reachable callstack from the given request.

State requests

val equality_class : Frama_c_kernel.Cil_types.exp -> request -> Frama_c_kernel.Cil_types.exp list result

Returns the list of expressions which have been inferred to be equal to the given expression by the Equality domain.

val get_cvalue_model : request -> Frama_c_kernel.Cvalue.Model.t

Returns the Cvalue state. Error cases are converted into the bottom or top cvalue state accordingly.

val get_cvalue_model_result : request -> Frama_c_kernel.Cvalue.Model.t result

Returns the Cvalue model.

val print_states : ?filter:Frama_c_kernel.Base.Hptset.t -> request -> (string * string) list

Returns a textual representation of the internal domain states for the given request. If filter is provided, states are filtered on the given bases (for domains that support this feature). Returns a list of pair (name, state) for all available domains.

Dependencies

val expr_deps : Frama_c_kernel.Cil_types.exp -> request -> Frama_c_kernel.Locations.Zone.t

Computes (an overapproximation of) the memory zones that must be read to evaluate the given expression, including all adresses computations.

val lval_deps : Frama_c_kernel.Cil_types.lval -> request -> Frama_c_kernel.Locations.Zone.t

Computes (an overapproximation of) the memory zones that must be read to evaluate the given lvalue, including the lvalue zone itself.

val address_deps : Frama_c_kernel.Cil_types.lval -> request -> Frama_c_kernel.Locations.Zone.t

Computes (an overapproximation of) the memory zones that must be read to evaluate the given lvalue, excluding the lvalue zone itself.

type taint =

| Direct
(*
Direct data dependency from values provided by the attacker to the given memory zone, meaning that the attacker may be able to alter its value.
*)
| Indirect
(*
Indirect dependency from values provided by the attacker to the given memory zone. The attacker cannot directly alter this memory, but he may be able to impact on the path by which its value is computed.
*)
| Untainted
(*
No taint: the given memory zone cannot be modified by the attacker.
*)

Taint of a memory zone, according to the taint domain.

val is_tainted : Frama_c_kernel.Locations.Zone.t -> request -> (taint, error) Frama_c_kernel.Result.t

Evaluates the taint of a given memory zone, according to the taint domain. Returns an error if the taint domain was not enabled.

val expr_dependencies : Frama_c_kernel.Cil_types.exp -> request -> Deps.t

Computes (an overapproximation of) the memory dependencies of an expression.

Evaluation

val eval_var : Frama_c_kernel.Cil_types.varinfo -> request -> value evaluation

Returns (an overapproximation of) the possible values of the variable.

val eval_lval : Frama_c_kernel.Cil_types.lval -> request -> value evaluation

Returns (an overapproximation of) the possible values of the lvalue.

val eval_exp : Frama_c_kernel.Cil_types.exp -> request -> value evaluation

Returns (an overapproximation of) the possible values of the expression.

val eval_address : ?for_writing:bool -> Frama_c_kernel.Cil_types.lval -> request -> address evaluation

Returns (an overapproximation of) the possible addresses of the lvalue.

val eval_callee : Frama_c_kernel.Cil_types.exp -> request -> Frama_c_kernel.Kernel_function.t list result

Returns the kernel functions into which the given expression may evaluate. If the callee expression doesn't always evaluate to a function, those spurious values are ignored. If it always evaluate to a non-function value then the returned list is empty. Raises Stdlib.Invalid_argument if the callee expression is not an lvalue without offset. Also see callee for a function which applies directly on Call statements.

Evaluated values conversion

In all functions below, if the abstract value inferred by Eva does not fit in the required type, Error Top is returned, as Top is the only possible over-approximation of the request.

val as_int : value evaluation -> int result

Converts the value into a singleton ocaml int.

val as_integer : value evaluation -> Frama_c_kernel.Integer.t result

Converts the value into a singleton unbounded integer.

val as_float : value evaluation -> float result

Converts the value into a floating point number.

val as_ival : value evaluation -> Frama_c_kernel.Ival.t result

Converts the value into a C number abstraction.

val as_fval : value evaluation -> Frama_c_kernel.Fval.t result

Converts the value into a floating point abstraction.

val as_cvalue : value evaluation -> Frama_c_kernel.Cvalue.V.t

Converts the value into a Cvalue abstraction. Converts error cases into bottom and top values accordingly.

val as_cvalue_result : value evaluation -> Frama_c_kernel.Cvalue.V.t result

Converts the value into a Cvalue abstraction.

val as_cvalue_or_uninitialized : value evaluation -> Frama_c_kernel.Cvalue.V_Or_Uninitialized.t

Converts the value into a Cvalue abstraction with 'undefined' and 'escaping addresses' flags.

val as_location : address evaluation -> Frama_c_kernel.Locations.location

Converts into a C location abstraction. Error cases are converted into bottom or top locations accordingly.

val as_location_result : address evaluation -> Frama_c_kernel.Locations.location result

Converts into a C location abstraction.

val as_zone : address evaluation -> Frama_c_kernel.Locations.Zone.t

Converts into a Zone. Error cases are converted into bottom or top zones accordingly.

val as_zone_result : address evaluation -> Frama_c_kernel.Locations.Zone.t result

Converts into a Zone result.

val as_precise_loc : address evaluation -> Frama_c_kernel.Precise_locs.precise_location

Converts into a C location abstraction. Error cases are converted into bottom or top locations accordingly.

val as_precise_loc_result : address evaluation -> Frama_c_kernel.Precise_locs.precise_location result

Converts into a C location abstraction.

Evaluation properties

val is_singleton : 'a evaluation -> bool

Does the evaluated abstraction represents only one possible C value or memory location?

val is_initialized : value evaluation -> bool

Returns whether the evaluated value is initialized or not. If the value have been evaluated from a Cil expression, it is always initialized.

val alarms : 'a evaluation -> Frama_c_kernel.Alarms.t list

Returns the set of alarms emitted during the evaluation.

Reachability

val is_empty : request -> bool

Returns true if there are no reachable states for the given request.

val is_bottom : 'a evaluation -> bool

Returns true if an evaluation leads to bottom, i.e. if the given expression or lvalue cannot be evaluated to a valid result for the given request.

val is_called : Frama_c_kernel.Cil_types.kernel_function -> bool

Returns true if the function has been analyzed.

val is_reachable : Frama_c_kernel.Cil_types.stmt -> bool

Returns true if the statement has been reached by the analysis.

val is_reachable_kinstr : Frama_c_kernel.Cil_types.kinstr -> bool

Returns true if the statement has been reached by the analysis, or if the main function has been analyzed for Kglobal.

val condition_truth_value : Frama_c_kernel.Cil_types.stmt -> bool * bool

Provided stmt is an 'if' construct, fst (condition_truth_value stmt) (resp. snd) is true if and only if the condition of the 'if' has been evaluated to true (resp. false) at least once during the analysis.

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

Returns the list of inferred callers of the given function.

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

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

val callee : Frama_c_kernel.Cil_types.stmt -> Frama_c_kernel.Kernel_function.t list

Returns the kernel functions called in the given statement. If the callee expression doesn't always evaluate to a function, those spurious values are ignored. If it always evaluate to a non-function value then the returned list is empty. Raises Stdlib.Invalid_argument if the statement is not a Call instruction or a Local_init with ConsInit initializer.

Frama-C API - Results

Frama-C API - `Results`