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 summary 
Summary of the analysis of a function. Useful at a call site.
module Summary: Datatype.S  with type t = summary
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 summary = summary 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, summary, value) Eval.call_result
include Abstract_domain.Logic

Miscellaneous


val open_block : Cil_types.fundec -> Cil_types.block -> body:bool -> t -> t
Scoping: abstract transformers for entering and exiting blocks. fundec is the englobing function, and body is true if the block is the body of fundec. (Otherwise, the block delimits an inner scope of fundec.) The interpreter assumes the locals of the block enter or leave the scope when these two functions are called, and the variables block.blocals should be added or removed from the abstract state here.
val close_block : Cil_types.fundec -> Cil_types.block -> body:bool -> 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