Frama-C API - `Minimal`

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 : Frama_c_kernel.Cil_types.kernel_function -> Frama_c_kernel.Cil_types.stmt -> t -> t -> t

Transfer functions.

val assign : pos:Position.t -> Eval.lval -> Eval.exp -> t -> t Eval.or_bottom

val assume : pos:Position.t -> Eval.exp -> bool -> t -> t Eval.or_bottom

val start_call : pos:Position.local -> simple_call -> t -> t

val finalize_call : pos:Position.local -> simple_call -> pre:t -> post:t -> t Eval.or_bottom

Initialization of variables.

val empty : unit -> t

val initialize_variable : Eval.lval -> initialized:bool -> Abstract_domain.init_value -> t -> t

val enter_scope : Abstract_domain.variable_kind -> Frama_c_kernel.Cil_types.varinfo list -> t -> t

val leave_scope : Frama_c_kernel.Cil_types.kernel_function -> Frama_c_kernel.Cil_types.varinfo list -> t -> t

Pretty printers.

val pretty : Stdlib.Format.formatter -> t -> unit

Frama-C API - Minimal