Module type Simpler_domains.Simple_Cvalue

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.

val extract_expr : t -> Cil_types.exp -> Simpler_domains.cvalue Eval.or_bottom
val extract_lval : t ->
Cil_types.lval ->
Cil_types.typ ->
Simpler_domains.precise_loc -> Simpler_domains.cvalue Eval.or_bottom

Transfer functions.

val assign : Cil_types.kinstr ->
Precise_locs.precise_location Eval.left_value ->
Cil_types.exp ->
(Simpler_domains.precise_loc, Simpler_domains.cvalue) 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 ->
(Simpler_domains.precise_loc, Simpler_domains.cvalue) Eval.call ->
Simpler_domains.cvalue_valuation -> t -> t
val finalize_call : Cil_types.stmt ->
(Simpler_domains.precise_loc, Simpler_domains.cvalue) Eval.call ->
pre:t -> post:t -> t 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 -> Stdlib.Format.formatter -> Cil_types.exp -> unit

Pretty printer.