Module Db.Value

module Value: sig .. end
The Value analysis itself.
See also internal documentation.

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 Pervasives.ref
Emitter used by Value to emit statuses
val self : State.t
Internal state of the value analysis from projects viewpoint.
Consult the Plugin Development Guide for additional details.
val mark_as_computed : unit -> unit
Indicate that the value analysis has been done already.
val compute : (unit -> unit) Pervasives.ref
Compute the value analysis using the entry point of the current project. You may set it with Globals.set_entry_point.
Raises Consult the Plugin Development Guide for additional details.
val is_computed : unit -> bool
Return true iff the value analysis has been done.
Consult the Plugin Development Guide for additional details.
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_sig = state ->
(Cil_types.exp * Cvalue.V.t * Cvalue.V_Offsetmap.t) list ->
Value_types.call_result
Type for a Value builtin function
val register_builtin : (string -> ?replace:string -> builtin_sig -> unit) Pervasives.ref
!register_builtin name ?replace f registers an abstract function f to use everytime a C function named name is called in the program. If replace is supplied and option -val-builtins-auto is active, calls to replace will also be substituted by the builtin. See also option -val-builtin
val registered_builtins : (unit -> (string * builtin_sig) list) Pervasives.ref
Returns a list of the pairs (name, builtin_sig) registered via register_builtin.
Since Aluminium-20160501
val mem_builtin : (string -> bool) Pervasives.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) Pervasives.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
Returns true if the initial state for globals used by the value analysis has been supplied by the user (through globals_set_initial_state), or false if it is automatically computed by the value analysis

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.
Consult the Plugin Development Guide for additional details.
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)
Pervasives.ref
val eval_expr : (?with_alarms:CilE.warn_mode -> state -> Cil_types.exp -> t)
Pervasives.ref
val eval_expr_with_state : (?with_alarms:CilE.warn_mode ->
state -> Cil_types.exp -> state * t)
Pervasives.ref
val reduce_by_cond : (state -> Cil_types.exp -> bool -> state) Pervasives.ref
val find_lv_plus : (Cvalue.Model.t -> Cil_types.exp -> (Cil_types.lval * Ival.t) list)
Pervasives.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)
Pervasives.ref
val expr_to_kernel_function_state : (state ->
deps:Locations.Zone.t option ->
Cil_types.exp -> Locations.Zone.t * Kernel_function.Hptset.t)
Pervasives.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.
Raises Not_a_call if the statement is not a call.
val valid_behaviors : (Cil_types.kernel_function -> state -> Cil_types.funbehavior list)
Pervasives.ref
val add_formals_to_state : (state ->
Cil_types.kernel_function -> Cil_types.exp list -> state)
Pervasives.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
Consult the Plugin Development Guide for additional details.
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.
Raises Void_Function if the function does not return any value.
val is_called : (Cil_types.kernel_function -> bool) Pervasives.ref
val callers : (Cil_types.kernel_function ->
(Cil_types.kernel_function * Cil_types.stmt list) list)
Pervasives.ref
Returns the list of callers with their call sites. Each function is present only once in the list.

State before a kinstr


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

Locations of left values


val lval_to_loc : (Cil_types.kinstr ->
?with_alarms:CilE.warn_mode -> Cil_types.lval -> Locations.location)
Pervasives.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)
Pervasives.ref
val lval_to_loc_with_deps_state : (state ->
deps:Locations.Zone.t ->
Cil_types.lval -> Locations.Zone.t * Locations.location)
Pervasives.ref
val lval_to_loc_state : (state -> Cil_types.lval -> Locations.location) Pervasives.ref
val lval_to_offsetmap : (Cil_types.kinstr ->
?with_alarms:CilE.warn_mode -> Cil_types.lval -> Cvalue.V_Offsetmap.t option)
Pervasives.ref
val lval_to_offsetmap_state : (state -> Cil_types.lval -> Cvalue.V_Offsetmap.t option)
Pervasives.ref
Since Carbon-20110201
val lval_to_zone : (Cil_types.kinstr ->
?with_alarms:CilE.warn_mode -> Cil_types.lval -> Locations.Zone.t)
Pervasives.ref
val lval_to_zone_state : (state -> Cil_types.lval -> Locations.Zone.t) Pervasives.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)
Pervasives.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)
Pervasives.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)
Pervasives.ref
val assigns_inputs_to_zone : (state -> Cil_types.assigns -> Locations.Zone.t) Pervasives.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)
Pervasives.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)
Pervasives.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)
Pervasives.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) Pervasives.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) Pervasives.ref

Pretty printing


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