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 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
Pretty printers.
val pretty : Format.formatter -> t -> unit
val show_expr : t -> Format.formatter -> Cil_types.exp -> unit