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 ->
       ?clear_formals:bool ->
       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. 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

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_types.kinstr ->
       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 ->
       call_kinstr:Cil_types.kinstr ->
       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.

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