Db.Value
Deprecated module: use the Eva.mli API instead.
type state = Cvalue.Model.t
Internal state of the value analysis.
type t = Cvalue.V.t
Internal representation of a value.
val emitter : Emitter.t Stdlib.ref
Emitter used by Value to emit statuses
val proxy : State_builder.Proxy.t
val self : State.t
Internal state of the value analysis from projects viewpoint.
Compute the value analysis using the entry point of the current project. You may set it with Globals.set_entry_point
.
module Table_By_Callstack :
State_builder.Hashtbl
with type key = Cil_types.stmt
and type data = state Value_types.Callstack.Hashtbl.t
Table containing the results of the value analysis, ie. the state before the evaluation of each reachable statement.
module AfterTable_By_Callstack :
State_builder.Hashtbl
with type key = Cil_types.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. Filled only if Value_parameters.ResultsAfter
is set.
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.
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.
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.
val fun_get_args : unit -> t list option
For this function, the result None
means that default values are used for the 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)
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.
val globals_state : unit -> state
Initial state used by the analysis
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
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.
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
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
val is_accessible : Cil_types.kinstr -> bool
val is_reachable : state -> bool
val is_reachable_stmt : Cil_types.stmt -> bool
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
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
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
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 Cil_datatype.Stmt.Hashtbl.t Stdlib.Lazy.t
module Record_Value_Superposition_Callbacks :
Hook.Iter_hook
with type param =
callstack * state list Cil_datatype.Stmt.Hashtbl.t Stdlib.Lazy.t
module Record_Value_After_Callbacks :
Hook.Iter_hook
with type param =
callstack * state Cil_datatype.Stmt.Hashtbl.t Stdlib.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. state
is the state before the call.
module Call_Type_Value_Callbacks :
Hook.Iter_hook
with type param =
[ `Builtin of Value_types.call_froms
| `Spec of Cil_types.funspec
| `Def
| `Memexec ]
* state
* callstack
Actions to perform at each treatment of a "call" statement. state
is the state before the call.
module Compute_Statement_Callbacks :
Hook.Iter_hook with type param = Cil_types.stmt * callstack * state list
Actions to perform whenever a statement is handled.
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