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
val approximate_call : Cil_types.stmt ->
Simpler_domains.simple_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

Pretty printers.

val pretty : Format.formatter -> t -> unit
val show_expr : t -> Format.formatter -> Cil_types.exp -> unit