Module type Abstract_domain.S

module type S = sig .. end
Signature for the abstract domains of the analysis.

type state 
include Datatype.S_with_collections
include Abstract_domain.Lattice

Lattice Structure


include Abstract_domain.Queries

Queries


type return 
Abstraction of the return value of a function. Allows information to flow from the return statement of a called function to the assignment of the call site.
module Return: Datatype.S  with type t = return
Datatypes

Transfer Functions


module Transfer: 
functor (Valuation : Abstract_domain.Valuation with type value = value and type origin = origin and type loc = location) -> Abstract_domain.Transfer with type state = t and type return = return and type value = value and type location = location and type valuation = Valuation.t
Transfer functions from the result of evaluations.

Logic


val compute_using_specification : Cil_types.kinstr ->
Cil_types.kernel_function * Cil_types.funspec ->
t -> (t, return, value) Eval.call_result
include Abstract_domain.Logic

Miscellaneous


val enter_scope : Cil_types.kernel_function -> Cil_types.varinfo list -> t -> t
Scoping: abstract transformers for entering and exiting blocks. kf is the englobing function, and the variables of the list vars should be added or removed from the abstract state here. Note that the formals of a function enter the scope through the transfer function Abstract_domain.Transfer.start_call, but leave it through a call to Abstract_domain.S.leave_scope.
val leave_scope : Cil_types.kernel_function -> Cil_types.varinfo list -> t -> t
val empty : unit -> t
Initialization
val initialize_var : t -> Cil_types.lval -> location -> (value * bool) Eval.or_bottom -> t
val initialize_var_using_type : t -> Cil_types.varinfo -> t
val global_state : unit -> t Eval.or_bottom option
val filter_by_bases : Base.Hptset.t -> t -> t
Mem exec.
val reuse : current_input:t -> previous_output:t -> t