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
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 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 ->
value Eval.call ->
Cil_types.funspec ->
state -> state list Eval.or_bottom
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 enter_loop : Cil_types.stmt -> state -> state
val incr_loop_counter : Cil_types.stmt -> state -> state
val leave_loop : Cil_types.stmt -> state -> state
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