Frama-C:
Plug-ins:
Libraries:

Frama-C API - Additive

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

Unique name of the datatype.

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.

The field over which the abstraction is defined.

module Scalar = Scalar
type scalar = Scalar.t

The monad used to encode context dependent computations.

module Computation = Computation
type 'a computation = 'a Computation.t

Constants and constructors.

val zero : t
val one : t
val singleton : scalar -> t

The call singleton r returns the abstract representation of the singleton subset containing r.

val between : scalar -> scalar -> t

The call between l r returns the abstract representation of the subset containing all scalars between l and u included.

Lattice structure.

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

Projection into an interval.

The lower and upper functions are provided as convenience.

val lower : t -> scalar
val upper : t -> scalar

Arithmetic operations.

val neg : t computation -> t computation
val sqrt : t computation -> t computation

Backward reductions.

val backward_left_less_than : left:t -> right:t -> t Frama_c_kernel.Lattice_bounds.or_bottom

The call backward_left_less_than ~left ~right returns a reduced abstraction of left based on the assumption that left <= right. If the assumption is wrong because no concrete element of left can possibly be less than any concrete element of right, the function must return `Bottom.

val backward_left_greater_than : left:t -> right:t -> t Frama_c_kernel.Lattice_bounds.or_bottom

The call backward_left_greater_than ~left ~right returns a reduced abstraction of left based on the assumption that left >= right. If the assumption is wrong because no concrete element of left can possibly be greater than any concrete element of right, the function must return `Bottom.