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