Module type Simpler_domains.Minimal

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