module Eval_funs:sig
..end
Value analysis of entire functions. Nothing is exported, but this
module fills Db.Value.compute
val dkey : Log.category
val compute_using_body : Kernel_function.t * Cil_types.fundec ->
call_kinstr:Cil_types.kinstr ->
with_formals:Cvalue.Model.t -> Value_types.call_result
kf
in state with_formals
according to the body f
of kf
.
Checks the preconditions of kf
, assuming the call took place at
call_kinstr
. The postconditions are checked within the call to
Computer.compute
.val compute_assigns : Kernel_function.t ->
Eval_annots.ActiveBehaviors.t ->
bool ->
with_formals:Cvalue.Model.t ->
Cil_types.varinfo option * Cvalue.Model.t * Base.SetLattice.t
kf
active according to active_behaviors
in
the state with_formals
.val compute_using_specification : Kernel_function.t * Cil_types.funspec ->
?clear_formals:bool ->
call_kinstr:Cil_types.kinstr ->
with_formals:Cvalue.Model.t -> unit -> Value_types.call_result
kf
in state with_formals
, first by reducing by the
preconditions, then by evaluating the assigns, then by reducing
by the post-conditions. The resulting states contain formals only
if clear_formals
is false.val compute_using_spec_or_body : with_formals:Cvalue.Model.t ->
call_kinstr:Cil_types.kinstr ->
show_progress:bool -> Kernel_function.t -> Value_types.call_result
kf
in the state with_formals
. The evaluation will
be done either using the body of kf
or its specification, depending
on whether the body exists and on option -val-use-spec
. call_kinstr
is the instruction at which the call takes place, and is used to update
the statuses of the preconditions of kf
. If show_progress
is true,
the callstack and additional information are printed.val compute_from_entry_point : unit -> unit
-lib-entry
and the options of Value governing
the shape of this state.val compute_maybe_builtin : Kernel_function.t ->
state:Db.Value.state ->
(Cil_types.exp * Cvalue.V_Offsetmap.t) list -> Value_types.call_result option
kf
in state state
. actuals
are
the arguments of kf
, and have not been bound to its formals. Returns
None
if the call must be computed using the Cil function for kf
.val compute_non_recursive_call : Kernel_function.t ->
call_kinstr:Cil_types.kinstr ->
Cvalue.Model.t ->
(Cil_types.exp * Cvalue.Model.offsetmap) list -> Value_types.call_result
kf
from call_kinstr
, assuming kf
is not yet present
in the callstack. In state
, the value of actuals in actuals
are not
yet bound to formals.val compute_recursive_call : Kernel_function.t ->
call_kinstr:Cil_types.kinstr ->
Cvalue.Model.t ->
(Cil_types.exp * Cvalue.Model.offsetmap) list -> Value_types.call_result
val compute_call : Kernel_function.t ->
call_kinstr:Cil_types.kinstr ->
Cvalue.Model.t ->
(Cil_types.exp * Cvalue.Model.offsetmap) list -> Value_types.call_result
kf
, called from call_kinstr
, in the state state
. In
this state, the value of actuals in actuals
are not yet bound to formals.val floats_ok : unit -> bool
val options_ok : unit -> unit
val check : unit -> unit
val generate_specs : unit -> unit
val pre : unit -> unit
val post_cleanup : aborted:bool -> unit
val force_compute : unit -> unit
val _self : State.t