module type Simple_Cvalue = sig
.. end
A simple interface allowing the abstract domain to use the value and
location abstractions computed by the other domains. Only the
Cvalue.V
and the the
Precise_locs
abstractions are available in this interface, on
the transfer functions for assignment, assumption and at the call sites. On
the other hand, the abstract domain cannot assist the computation of these
value and location abstractions. The communication is thus unidirectional,
from other domains to these simpler domains.
include Datatype.S
Lattice structure.
val top : t
val is_included : t -> t -> bool
val join : t -> t -> t
val widen : Cil_types.kernel_function -> Cil_types.stmt -> t -> t -> t
Query functions.
: t -> Cil_types.exp -> Cvalue.V.t Eval.or_bottom
: t ->
Cil_types.lval ->
Cil_types.typ -> Precise_locs.precise_location -> Cvalue.V.t Eval.or_bottom
Transfer functions.
val assign : Cil_types.kinstr ->
Precise_locs.precise_location Eval.left_value ->
Cil_types.exp ->
Cvalue.V.t Eval.assigned ->
Simpler_domains.cvalue_valuation -> t -> t Eval.or_bottom
val assume : Cil_types.stmt ->
Cil_types.exp ->
bool -> Simpler_domains.cvalue_valuation -> t -> t Eval.or_bottom
val start_call : Cil_types.stmt ->
Cvalue.V.t Eval.call -> Simpler_domains.cvalue_valuation -> t -> t
val finalize_call : Cil_types.stmt -> Cvalue.V.t Eval.call -> pre:t -> post:t -> t Eval.or_bottom
val approximate_call : Cil_types.stmt -> Cvalue.V.t Eval.call -> t -> t list Eval.or_bottom
Initialization of variables.
val empty : unit -> t
val introduce_globals : Cil_types.varinfo list -> t -> t
val initialize_variable : Cil_types.lval -> initialized:bool -> Abstract_domain.init_value -> t -> t
val enter_scope : Cil_types.kernel_function -> Cil_types.varinfo list -> t -> t
val leave_scope : Cil_types.kernel_function -> Cil_types.varinfo list -> t -> t
val show_expr : t -> Format.formatter -> Cil_types.exp -> unit
Pretty printer.