module type Minimal =sig
..end
Simplest interface for an abstract domain. No exchange of information with the other abstractions of Eva.
type
t
val name : string
val compare : t -> t -> int
val hash : t -> int
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
Transfer functions.
val assign : Cil_types.kinstr ->
Cil_types.lval ->
Cil_types.exp ->
t -> t Eval.or_bottom
val assume : Cil_types.stmt ->
Cil_types.exp ->
bool -> t -> t Eval.or_bottom
val start_call : Cil_types.stmt ->
Simpler_domains.simple_call ->
t -> t
val finalize_call : Cil_types.stmt ->
Simpler_domains.simple_call ->
pre:t ->
post:t -> t Eval.or_bottom
Initialization of variables.
val empty : unit -> t
val initialize_variable : Cil_types.lval ->
initialized:bool ->
Abstract_domain.init_value ->
t -> t
val enter_scope : Abstract_domain.variable_kind ->
Cil_types.varinfo list ->
t -> t
val leave_scope : Cil_types.kernel_function ->
Cil_types.varinfo list ->
t -> t
Pretty printers.
val pretty : Stdlib.Format.formatter -> t -> unit