Module Eval_funs

module Eval_funs: sig .. end
Value analysis of entire functions

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
Compute 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
Evaluate the assigns of kf active according to active_behaviors in the state with_formals.
val compute_using_specification : Kernel_function.t * Cil_types.funspec ->
call_kinstr:Cil_types.kinstr ->
with_formals:Cvalue.Model.t -> unit -> Value_types.call_result
Evaluate kf in state with_formals, first by reducing by the preconditions, then by evaluating the assigns, then by reducing by the post-conditions.
val compute_using_spec_or_body : with_formals:Cvalue.Model.t ->
call_kinstr:Cil_datatype.Kinstr.t ->
show_progress:bool -> Kernel_function.Set.elt -> Value_types.call_result
Compute a call to 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
Compute a call to the main function. The initial state is generated according to options such as -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
Compute a call to a possible builtin 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_datatype.Kinstr.t ->
Cvalue.Model.t ->
(Cil_types.exp * Cvalue.Model.offsetmap) list -> Value_types.call_result
Compute a call to 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 ->
recursive:bool ->
call_kinstr:Cil_datatype.Kinstr.t ->
Cvalue.Model.t ->
(Cil_types.exp * Cvalue.Model.offsetmap) list -> Value_types.call_result
Compute a call to kf, called from call_kinstr, in the state state. In this state, the value of actuals in actuals are not yet bound to formals. recursive means that the call is recursive.
val floats_ok : unit -> bool
val need_assigns : Cil_types.kernel_function -> 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