module Value:sig
..end
The Value analysis itself.
typestate =
Cvalue.Model.t
Internal state of the value analysis.
typet =
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.
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
.
Globals.No_such_entry_point
if the entry point is incorrectDb.Value.Incorrect_number_of_arguments
if some arguments are
specified for the entry point using Db.Value.fun_set_args
, and
an incorrect number of them is given.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.
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. 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)
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
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 analysisState 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
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.
Not_a_call
if the statement is not a 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
exception Void_Function
val find_return_loc : Cil_types.kernel_function -> Locations.location
Return the location of the returned lvalue of the given function.
Void_Function
if the function does not return any value.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
Evaluation of logic terms and predicates
typecallstack =
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_froms | `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
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