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