Frama-C:
Plug-ins:
Libraries:

Frama-C API - Ival

Arithmetic lattices. The interfaces of this module may change between Frama-C versions. Contact us if you need stable APIs.

type t

General guidelines of this module

  • Functions suffixed by _int expect arguments that are integers. Hence, they will fail on an ival with constructor Float. Conversely, _float suffixed functions expect float arguments: the constructor Float, or the singleton set [| Int.zero |] , that can be tested by is_zero.
  • see the comment in Lattice_type about over- and under-approximations, and exact operations.
include Datatype.S_with_collections with type t := t
include Datatype.S with type t := t
include Datatype.S_no_copy with type t := t
include Datatype.Ty with type t := t
module Set : Datatype.Set with type elt = t
module Map : Datatype.Map with type key = t
module Hashtbl : Datatype.Hashtbl with type key = t
include Lattice_type.Full_AI_Lattice_with_cardinality with type t := t
include Lattice_type.AI_Lattice_with_cardinal_one with type t := t
include Lattice_type.Bounded_Join_Semi_Lattice with type t := t
include Lattice_type.Join_Semi_Lattice with type t := t

datatype of element of the lattice

include Datatype.S with type t := t
include Datatype.S_no_copy with type t := t
include Datatype.Ty with type t := t
val ty : t Type.t
val name : string

Unique name of the datatype.

val descr : t Descr.t

Datatype descriptor.

val packed_descr : Structural_descr.pack

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 : (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 join : t -> t -> t

over-approximation of union

val is_included : t -> t -> bool

is first argument included in the second?

val bottom : t

smallest element

include Lattice_type.With_Top with type t := t
val top : t

largest element

include Lattice_type.With_Cardinal_One with type t := t
include Lattice_type.With_Narrow with type t := t
val narrow : t -> t -> t

over-approximation of intersection

include Lattice_type.With_Under_Approximation with type t := t

under-approximation of union

val meet : t -> t -> t

under-approximation of intersection

include Lattice_type.With_Intersects with type t := t
val intersects : t -> t -> bool

intersects t1 t2 returns true iff the intersection of t1 and t2 is non-empty.

include Lattice_type.With_Diff with type t := t
val diff : t -> t -> t

diff t1 t2 is an over-approximation of t1-t2. t2 must be an under-approximation or exact.

include Lattice_type.With_Diff_One with type t := t
val diff_if_one : t -> t -> t

diff_if_one t1 t2 is an over-approximation of t1-t2.

  • returns

    t1 if t2 is not a singleton.

include Lattice_type.With_Enumeration with type t := t

Widening hints: set of relevant integer and floating-point thresholds.

val widen : ?size:Integer.t -> ?hint:widen_hint -> t -> t -> t

widen ~size ~hint t1 t2 is an over-approximation of join t1 t2. size is the size (in bits) of the widened value, and hint is a set of relevant thresholds.

val is_bottom : t -> bool
val is_float : t -> bool
val is_int : t -> bool
val add_int : t -> t -> t

Addition of two integer (ie. not Float) ivals.

val add_int_under : t -> t -> t

Underapproximation of the same operation

val add_singleton_int : Integer.t -> t -> t

Addition of an integer ival with an integer. Exact operation.

val neg_int : t -> t

Negation of an integer ival. Exact operation.

val abs_int : t -> t

Absolute value of an integer.

val sub_int : t -> t -> t
val sub_int_under : t -> t -> t
val min_int : t -> Integer.t option

A None result means the argument is unbounded. Raises Error_Bottom if the argument is bottom.

val max_int : t -> Integer.t option

A None result means the argument is unbounded. Raises Error_Bottom if the argument is bottom.

val min_max_r_mod : t -> Integer.t option * Integer.t option * Integer.t * Integer.t
val min_and_max : t -> Integer.t option * Integer.t option

Returns the minimal and maximal integers represented by an ival. None means the argument is unbounded.

val min_and_max_float : t -> (Fval.F.t * Fval.F.t) option * bool

returns the bounds of the float interval, (or None if the argument is exactly NaN), and a boolean indicating the possibility that the value may be NaN.

val bitwise_and : t -> t -> t
val bitwise_or : t -> t -> t
val bitwise_xor : t -> t -> t
val bitwise_signed_not : t -> t
val bitwise_unsigned_not : size:int -> t -> t
val bitwise_not : size:int -> signed:bool -> t -> t
val zero : t

The lattice element that contains only the integer 0.

val one : t

The lattice element that contains only the integer 1.

val minus_one : t

The lattice element that contains only the integer -1.

val zero_or_one : t

The lattice element that contains only the integers 0 and 1.

val positive_integers : t

The lattice element that contains exactly the positive or null integers

val negative_integers : t

The lattice element that contains exactly the negative or null integers

val float_zeros : t

The lattice element containing exactly -0. and 0.

val is_zero : t -> bool
val is_one : t -> bool
val contains_zero : t -> bool

contains the zero value (including -0. for floating-point ranges)

val contains_non_zero : t -> bool
val top_float : t
val top_single_precision_float : t
val project_float : t -> Fval.t

Should be used only when we know it is a float

Building Ival

val inject_singleton : Integer.t -> t
val inject_float : Fval.t -> t
val inject_float_interval : float -> float -> t
val inject_range : Integer.t option -> Integer.t option -> t

None means unbounded. The interval is inclusive.

val inject_interval : min:Integer.t option -> max:Integer.t option -> rem:Integer.t -> modu:Integer.t -> t

Builds the set of integers between min and max included and congruent to rem modulo modulo. For min and max, None is the corresponding infinity. Checks that modu > 0 and 0 <= rest < modu, and fails otherwise.

Cardinality

val cardinal_zero_or_one : t -> bool
val is_singleton_int : t -> bool
exception Not_Singleton_Int
val project_int_val : t -> Int_val.t option
val project_int : t -> Integer.t
  • raises Not_Singleton_Int

    when the cardinal of the argument is not 1, or if it is not an integer.

val is_small_set : t -> bool
val project_small_set : t -> Integer.t list option
val cardinal : t -> Integer.t option

cardinal v returns n if v has finite cardinal n, or None if the cardinal is not finite.

val cardinal_estimate : t -> size:Integer.t -> Integer.t

cardinal_estimate v ~size returns an estimation of the cardinal of v, knowing that v fits in size bits.

val cardinal_less_than : t -> int -> int

cardinal_less_than t n returns the cardinal of t is this cardinal is at most n.

val cardinal_is_less_than : t -> int -> bool

Same than cardinal_less_than but just return if it is the case.

val fold_int : (Integer.t -> 'a -> 'a) -> t -> 'a -> 'a

Iterate on the integer values of the ival in increasing order. Raise Abstract_interp.Error_Top if the argument is a float or a potentially infinite integer.

val fold_int_decrease : (Integer.t -> 'a -> 'a) -> t -> 'a -> 'a

Iterate on the integer values of the ival in decreasing order. Raise Abstract_Interp.Error_Top if the argument is a float or a potentially infinite integer.

val fold_enum : (t -> 'a -> 'a) -> t -> 'a -> 'a

Iterate on every value of the ival. Raise Abstract_interp.Error_Top if the argument is a non-singleton float or a potentially infinite integer.

val fold_int_bounds : (t -> 'a -> 'a) -> t -> 'a -> 'a

Given i an integer abstraction min..max, fold_int_bounds f i acc tries to apply f to min, max, and i' successively, where i' is i from which min and max have been removed. If min and/or max are infinite, f is called with an argument i' unreduced in the corresponding direction(s).

val to_int_seq : t -> Integer.t Stdlib.Seq.t

Builds a sequence of integer values of the ival in increasing order. The resulting sequence might be infinite.

  • raises {!Abstract_interp.Error_Top}

    if the argument is a floating-point interval or an infinite integer interval.

val subdivide : size:Integer.t -> t -> t * t

Subdivisions into two intervals

val has_greater_min_bound : t -> t -> int

has_greater_min_bound i1 i2 returns 1 if the interval i1 has a better minimum bound (i.e. greater) than the interval i2. i1 and i2 should not be bottom.

val has_smaller_max_bound : t -> t -> int

has_smaller_max_bound i1 i2 returns 1 if the interval i1 has a better maximum bound (i.e. lower) than the interval i2. i1 and i2 should not be bottom.

val scale : Integer.t -> t -> t

scale f v returns the interval of elements x * f for x in v. The operation is exact, except when v is a float.

val scale_div : pos:bool -> Integer.t -> t -> t

scale_div ~pos:false f v is an over-approximation of the set of elements x c_div f for x in v.

scale_div ~pos:true f v is an over-approximation of the set of elements x e_div f for x in v.

val scale_div_under : pos:bool -> Integer.t -> t -> t

scale_div_under ~pos:false f v is an under-approximation of the set of elements x c_div f for x in v.

scale_div_under ~pos:true f v is an under-approximation of the set of elements x e_div f for x in v.

val div : t -> t -> t

Integer division

val scale_rem : pos:bool -> Integer.t -> t -> t

scale_rem ~pos:false f v is an over-approximation of the set of elements x c_rem f for x in v.

scale_rem ~pos:true f v is an over-approximation of the set of elements x e_rem f for x in v.

val c_rem : t -> t -> t
val mul : t -> t -> t
val shift_left : t -> t -> t
val shift_right : t -> t -> t
val interp_boolean : contains_zero:bool -> contains_non_zero:bool -> t
val extract_bits : start:Integer.t -> stop:Integer.t -> size:Integer.t -> t -> t

Extract bits from start to stop from the given Ival, start and stop being included. size is the size of the entire ival.

val create_all_values : signed:bool -> size:int -> t
val all_values : size:Integer.t -> t -> bool

all_values ~size v returns true iff v contains all integer values representable in size bits.

val backward_mult_int_left : right:t -> result:t -> t option Lattice_bounds.or_bottom
val backward_comp_int_left : Abstract_interp.Comp.t -> t -> t -> t

backward_comp_int op l r reduces l into l' so that l' op r holds. l is assumed to be an integer

val backward_comp_float_left_true : Abstract_interp.Comp.t -> Fval.kind -> t -> t -> t
val backward_comp_float_left_false : Abstract_interp.Comp.t -> Fval.kind -> t -> t -> t

Same as backward_comp_int_left, except that the arguments should now be floating-point values.

val forward_comp_int : Abstract_interp.Comp.t -> t -> t -> Abstract_interp.Comp.result
val scale_int_base : Int_Base.t -> t -> t
val of_int : int -> t
val of_int64 : int64 -> t

Casts

val cast_int_to_int : size:Integer.t -> signed:bool -> t -> t
val cast_int_to_float : Fval.kind -> t -> t
val cast_float_to_int : signed:bool -> size:int -> t -> t

Casts the given float into an integer. NaN and out-of-bounds values are ignored.

val cast_float_to_float : Fval.kind -> t -> t

Cast the given float to the given size.

val cast_float_to_int_inverse : single_precision:bool -> t -> t

floating-point

val cast_int_to_float_inverse : single_precision:bool -> t -> t

integer

val reinterpret_as_float : Cil_types.fkind -> t -> t

Bitwise reinterpretation of the given value as a float of the given kind.

val reinterpret_as_int : size:Integer.t -> signed:bool -> t -> t

Bitwise reinterpretation of the given value, of size size, as an integer of the given signedness (and size).

val complement_int_under : size:int -> signed:bool -> t -> t Lattice_bounds.or_bottom

Returns an under-approximation of the integers of the given size and signedness that are *not* represented by the given ival.