Frama-C:
Plug-ins:
Libraries:

Frama-C API - Simple_Cvalue

A simple interface allowing the abstract domain to use the value and location abstractions computed by the other domains. Only the Cvalue.V and the the Precise_locs abstractions are available in this interface, on the transfer functions for assignment, assumption and at the call sites. On the other hand, the abstract domain cannot assist the computation of these value and location abstractions. The communication is thus unidirectional, from other domains to these simpler domains.

include Frama_c_kernel.Datatype.S
include Frama_c_kernel.Datatype.S_no_copy
include Frama_c_kernel.Datatype.Ty
type t
val datatype_name : string

Unique name of the datatype.

val datatype_descr : t Frama_c_kernel.Descr.t

Datatype descriptor.

Packed version of the descriptor.

val reprs : t list

List of representants of the descriptor.

val equal : t -> t -> bool

Equality: same spec than Stdlib.(=).

val compare : t -> t -> int

Comparison: same spec than Stdlib.compare.

val hash : t -> int

Hash function: same spec than Hashtbl.hash.

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

Pretty print each value in an user-friendly way.

val mem_project : (Frama_c_kernel.Project_skeleton.t -> bool) -> t -> bool

mem_project f x must return true iff there is a value p of type Project.t in x such that f p returns true.

val copy : t -> t

Deep copy: no possible sharing between x and copy x.

val name : string

Domain name

Lattice structure.

val top : t
val is_included : t -> t -> bool
val join : t -> t -> t

Query functions.

val extract_expr : t -> Eval.exp -> cvalue Eval.or_bottom
val extract_lval : t -> Eval.lval -> precise_loc -> cvalue Eval.or_bottom

Transfer functions.

val assume : pos:Position.t -> Eval.exp -> bool -> cvalue_valuation -> t -> t Eval.or_bottom
val start_call : pos:Position.local -> (precise_loc, cvalue) Eval.call -> cvalue_valuation -> t -> t
val finalize_call : pos:Position.local -> (precise_loc, cvalue) Eval.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