Module Db.Value

module Value: sig .. end

The Value analysis itself.


type state = Cvalue.Model.t 

Internal state of the value analysis.

type t = Cvalue.V.t 

Internal representation of a value.

exception Aborted
val emitter : Emitter.t Stdlib.ref

Emitter used by Value to emit statuses

val self : State.t

Internal state of the value analysis from projects viewpoint.

val mark_as_computed : unit -> unit

Indicate that the value analysis has been done already.

val compute : (unit -> unit) Stdlib.ref

Compute the value analysis using the entry point of the current project. You may set it with Globals.set_entry_point.

val is_computed : unit -> bool

Return true iff the value analysis has been done.

module Table_By_Callstack: State_builder.Hashtbl  with type key = stmt
                          and type data = state Value_types.Callstack.Hashtbl.t

Table containing the results of the value analysis, ie.

module AfterTable_By_Callstack: State_builder.Hashtbl  with type key = stmt
                          and type data = state Value_types.Callstack.Hashtbl.t

Table containing the state of the value analysis after the evaluation of each reachable and evaluable statement.

val ignored_recursive_call : Cil_types.kernel_function -> bool

This functions returns true if the value analysis found and ignored a recursive call to this function during the analysis.

val condition_truth_value : 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.

Parameterization

exception Outside_builtin_possibilities
type builtin_type = unit -> Cil_types.typ * Cil_types.typ list 
type builtin = state ->
(Cil_types.exp * Cvalue.V.t * Cvalue.V_Offsetmap.t) list ->
Value_types.call_result

Type for an Eva builtin function

val register_builtin : (string ->
?replace:string -> ?typ:builtin_type -> builtin -> unit)
Stdlib.ref

!register_builtin name ?replace ?typ f registers an abstract function f to use everytime a C function named name of type typ is called in the program. If replace is supplied and option -eva-builtins-auto is active, calls to replace will also be substituted by the builtin. See also option -eva-builtin

val registered_builtins : (unit -> (string * builtin) list) Stdlib.ref

Returns a list of the pairs (name, builtin) registered via register_builtin.

val mem_builtin : (string -> bool) Stdlib.ref

returns whether there is an abstract function registered by Db.Value.register_builtin with the given name.

val use_spec_instead_of_definition : (Cil_types.kernel_function -> bool) Stdlib.ref

To be called by derived analyses to determine if they must use the body of the function (if available), or only its spec. Used for value builtins, and option -val-use-spec.

Arguments of the main function

The functions below are related to the arguments that are passed to the function that is analysed by the value analysis. Specific arguments are set by fun_set_args. Arguments reset to default values when fun_use_default_args is called, when the ast is changed, or if the options -libentry or -main are changed.

val fun_set_args : t list -> unit

Specify the arguments to use. This function is not journalized, and will generate an error when the journal is replayed

val fun_use_default_args : unit -> unit
val fun_get_args : unit -> t list option

For this function, the result None means that default values are used for the arguments.

exception Incorrect_number_of_arguments

Raised by Db.Compute when the arguments set by fun_set_args are not coherent with the prototype of the function (if there are too few or too many of them)

Initial state of the analysis

The functions below are related to the value of the global variables when the value analysis is started. If globals_set_initial_state has not been called, the given state is used. A default state (which depends on the option -libentry) is used when globals_use_default_initial_state is called, or when the ast changes.

val globals_set_initial_state : state -> unit

Specify the initial state to use. This function is not journalized, and will generate an error when the journal is replayed

val globals_use_default_initial_state : unit -> unit
val globals_state : unit -> state

Initial state used by the analysis

val globals_use_supplied_state : unit -> bool

Getters

State of the analysis at various points

val get_initial_state : Cil_types.kernel_function -> state
val get_initial_state_callstack : Cil_types.kernel_function ->
state Value_types.Callstack.Hashtbl.t option
val get_state : ?after:bool -> Cil_types.kinstr -> state

after is false by default.

val get_stmt_state_callstack : after:bool ->
Cil_types.stmt -> state Value_types.Callstack.Hashtbl.t option
val get_stmt_state : ?after:bool -> Cil_types.stmt -> state

after is false by default.

val fold_stmt_state_callstack : (state -> 'a -> 'a) -> 'a -> after:bool -> Cil_types.stmt -> 'a
val fold_state_callstack : (state -> 'a -> 'a) -> 'a -> after:bool -> Cil_types.kinstr -> 'a
val find : state -> Locations.location -> t

Evaluations

val eval_lval : (?with_alarms:CilE.warn_mode ->
Locations.Zone.t option ->
state -> Cil_types.lval -> Locations.Zone.t option * t)
Stdlib.ref
val eval_expr : (?with_alarms:CilE.warn_mode -> state -> Cil_types.exp -> t)
Stdlib.ref
val eval_expr_with_state : (?with_alarms:CilE.warn_mode ->
state -> Cil_types.exp -> state * t)
Stdlib.ref
val reduce_by_cond : (state -> Cil_types.exp -> bool -> state) Stdlib.ref
val find_lv_plus : (Cvalue.Model.t -> Cil_types.exp -> (Cil_types.lval * Ival.t) list)
Stdlib.ref

returns the list of all decompositions of expr into the sum an lvalue and an interval.

Values and kernel functions

val expr_to_kernel_function : (Cil_types.kinstr ->
?with_alarms:CilE.warn_mode ->
deps:Locations.Zone.t option ->
Cil_types.exp -> Locations.Zone.t * Kernel_function.Hptset.t)
Stdlib.ref
val expr_to_kernel_function_state : (state ->
deps:Locations.Zone.t option ->
Cil_types.exp -> Locations.Zone.t * Kernel_function.Hptset.t)
Stdlib.ref
exception Not_a_call
val call_to_kernel_function : Cil_types.stmt -> Kernel_function.Hptset.t

Return the functions that can be called from this call.

val valid_behaviors : (Cil_types.kernel_function -> state -> Cil_types.funbehavior list)
Stdlib.ref
val add_formals_to_state : (state ->
Cil_types.kernel_function -> Cil_types.exp list -> state)
Stdlib.ref

add_formals_to_state state kf exps evaluates exps in state and binds them to the formal arguments of kf in the resulting state

Reachability

val is_accessible : Cil_types.kinstr -> bool
val is_reachable : state -> bool
val is_reachable_stmt : Cil_types.stmt -> bool

About kernel functions

exception Void_Function
val find_return_loc : Cil_types.kernel_function -> Locations.location

Return the location of the returned lvalue of the given function.

val is_called : (Cil_types.kernel_function -> bool) Stdlib.ref
val callers : (Cil_types.kernel_function ->
(Cil_types.kernel_function * Cil_types.stmt list) list)
Stdlib.ref

State before a kinstr

val access : (Cil_types.kinstr -> Cil_types.lval -> t) Stdlib.ref
val access_expr : (Cil_types.kinstr -> Cil_types.exp -> t) Stdlib.ref
val access_location : (Cil_types.kinstr -> Locations.location -> t) Stdlib.ref

Locations of left values

val lval_to_loc : (Cil_types.kinstr ->
?with_alarms:CilE.warn_mode -> Cil_types.lval -> Locations.location)
Stdlib.ref
val lval_to_loc_with_deps : (Cil_types.kinstr ->
?with_alarms:CilE.warn_mode ->
deps:Locations.Zone.t ->
Cil_types.lval -> Locations.Zone.t * Locations.location)
Stdlib.ref
val lval_to_loc_with_deps_state : (state ->
deps:Locations.Zone.t ->
Cil_types.lval -> Locations.Zone.t * Locations.location)
Stdlib.ref
val lval_to_loc_state : (state -> Cil_types.lval -> Locations.location) Stdlib.ref
val lval_to_offsetmap : (Cil_types.kinstr ->
?with_alarms:CilE.warn_mode -> Cil_types.lval -> Cvalue.V_Offsetmap.t option)
Stdlib.ref
val lval_to_offsetmap_state : (state -> Cil_types.lval -> Cvalue.V_Offsetmap.t option) Stdlib.ref
val lval_to_zone : (Cil_types.kinstr ->
?with_alarms:CilE.warn_mode -> Cil_types.lval -> Locations.Zone.t)
Stdlib.ref
val lval_to_zone_state : (state -> Cil_types.lval -> Locations.Zone.t) Stdlib.ref

Does not emit alarms.

val lval_to_zone_with_deps_state : (state ->
for_writing:bool ->
deps:Locations.Zone.t option ->
Cil_types.lval -> Locations.Zone.t * Locations.Zone.t * bool)
Stdlib.ref

lval_to_zone_with_deps_state state ~for_writing ~deps lv computes res_deps, zone_lv, exact, where res_deps are the memory zones needed to evaluate lv in state joined with deps. zone_lv contains the valid memory zones that correspond to the location that lv evaluates to in state. If for_writing is true, zone_lv is restricted to memory zones that are writable. exact indicates that lv evaluates to a valid location of cardinal at most one.

val lval_to_precise_loc_state : (?with_alarms:CilE.warn_mode ->
state ->
Cil_types.lval ->
state * Precise_locs.precise_location * Cil_types.typ)
Stdlib.ref
val lval_to_precise_loc_with_deps_state : (state ->
deps:Locations.Zone.t option ->
Cil_types.lval -> Locations.Zone.t * Precise_locs.precise_location)
Stdlib.ref
val assigns_inputs_to_zone : (state -> Cil_types.assigns -> Locations.Zone.t) Stdlib.ref

Evaluation of the \from clause of an assigns clause.

val assigns_outputs_to_zone : (state ->
result:Cil_types.varinfo option -> Cil_types.assigns -> Locations.Zone.t)
Stdlib.ref

Evaluation of the left part of assigns clause (without \from).

val assigns_outputs_to_locations : (state ->
result:Cil_types.varinfo option ->
Cil_types.assigns -> Locations.location list)
Stdlib.ref

Evaluation of the left part of assigns clause (without \from). Each assigns term results in one location.

val verify_assigns_froms : (Kernel_function.t -> pre:state -> Function_Froms.t -> unit)
Stdlib.ref

For internal use only. Evaluate the assigns clause of the given function in the given prestate, compare it with the computed froms, return warning and set statuses.

module Logic: sig .. end

Evaluation of logic terms and predicates

Callbacks

type callstack = Value_types.callstack 

Actions to perform at end of each function analysis. Not compatible with option -memexec-all

module Record_Value_Callbacks: Hook.Iter_hook  with type param = callstack * (state Stmt.Hashtbl.t) Lazy.t
module Record_Value_Superposition_Callbacks: Hook.Iter_hook  with type param = callstack * (state list Stmt.Hashtbl.t) Lazy.t
module Record_Value_After_Callbacks: Hook.Iter_hook  with type param = callstack * (state Stmt.Hashtbl.t) Lazy.t
val no_results : (Cil_types.fundec -> bool) Stdlib.ref

Returns true if the user has requested that no results should be recorded for this function. If possible, hooks registered on Record_Value_Callbacks and Record_Value_Callbacks_New should not force their lazy argument

module Call_Value_Callbacks: Hook.Iter_hook  with type param = state * callstack

Actions to perform at each treatment of a "call" statement.

module Call_Type_Value_Callbacks: Hook.Iter_hook  with type param =
    [`Builtin of Value_types.call_result | `Spec of funspec | `Def | `Memexec]
    * state * callstack

Actions to perform at each treatment of a "call" statement.

module Compute_Statement_Callbacks: Hook.Iter_hook  with type param = stmt * callstack * state list

Actions to perform whenever a statement is handled.

val rm_asserts : (unit -> unit) Stdlib.ref

Pretty printing

val pretty : Stdlib.Format.formatter -> t -> unit
val pretty_state : Stdlib.Format.formatter -> state -> unit
val display : (Stdlib.Format.formatter -> Cil_types.kernel_function -> unit) Stdlib.ref