Module `Framac_ival.Ival`Source

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

Sourcetype t = private

| Set of Abstract_interp.Int.t array
| Float of Fval.t
(*
Top(min, max, rem, modulo) represents the interval between min and max, congruent to rem modulo modulo. A value of None for min (resp. max) represents -infinity (resp. +infinity). modulo is > 0, and 0 <= rem < modulo.
Actual Top is thus represented by Top(None,None,Int.zero,Int.one)
*)
| Top of Abstract_interp.Int.t option * Abstract_interp.Int.t option * Abstract_interp.Int.t * Abstract_interp.Int.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.

Sourcemodule Widen_Hints : sig ... end

Sourcetype size_widen_hint = Integer.t

Sourcetype generic_widen_hint = Widen_Hints.t

include Datatype_sig.S with type t := t

Sourceval equal : t -> t -> bool

Any notion of equality is allowed, as long as it is an equivalence relation, and that if a == b, then equal a b.

Sourceval compare : t -> t -> int

compare is a total order, and should be compatible with equal.

Sourceval hash : t -> int

hash requires that equal values have the same hash.

Sourceval pretty : Format.formatter -> t -> unit

Sourceval top : t

Sourceval bottom : t

Sourceval narrow : t -> t -> t

Sourceval is_included : t -> t -> bool

Sourceval diff_if_one : t -> t -> t

Sourceval join : t -> t -> t

Sourceval widen : (Integer.t * Widen_Hints.t) -> t -> t -> t

Sourceval is_bottom : t -> bool

Sourceval overlaps : partial:bool -> size:Integer.t -> t -> t -> bool

Sourceval add_int : t -> t -> t

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

Sourceval add_int_under : t -> t -> t

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

Underapproximation of the same operation

Sourceval add_singleton_int : Integer.t -> t -> t

Underapproximation of the same operation

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

Sourceval neg_int : t -> t

Negation of an integer ival. Exact operation.

Sourceval sub_int : t -> t -> t

Negation of an integer ival. Exact operation.

Sourceval sub_int_under : t -> t -> t

Sourceval min_int : t -> Integer.t option

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

Sourceval max_int : t -> Integer.t option

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

Source

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

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

Sourceval 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.

raises Abstract_interp.Error_Bottom
if the argument is bottom.

Sourceval 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.

Sourceval bitwise_and : t -> t -> t

Sourceval bitwise_or : t -> t -> t

Sourceval bitwise_xor : t -> t -> t

Sourceval bitwise_signed_not : t -> t

Sourceval bitwise_unsigned_not : size:int -> t -> t

Sourceval bitwise_not : size:int -> signed:bool -> t -> t

Sourceval zero : t

The lattice element that contains only the integer 0.

Sourceval one : t

The lattice element that contains only the integer 0.

The lattice element that contains only the integer 1.

Sourceval minus_one : t

The lattice element that contains only the integer 1.

The lattice element that contains only the integer -1.

Sourceval zero_or_one : t

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

Sourceval positive_integers : t

The lattice element that contains exactly the positive or null integers

Sourceval negative_integers : t

The lattice element that contains exactly the negative or null integers

Sourceval float_zeros : t

The lattice element containing exactly -0. and 0.

Sourceval is_zero : t -> bool

Sourceval is_one : t -> bool

Sourceval contains_zero : t -> bool

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

Sourceval contains_non_zero : t -> bool

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

Sourceval top_float : t

Sourceval top_single_precision_float : t

Sourceval project_float : t -> Fval.t

Should be used only when we know it is a float

Building Ival

Sourceval inject_singleton : Integer.t -> t

Sourceval inject_float : Fval.t -> t

Sourceval inject_float_interval : float -> float -> t

Sourceval inject_range : Integer.t option -> Integer.t option -> t

None means unbounded. The interval is inclusive.

Source

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

Sourceval cardinal_zero_or_one : t -> bool

Sourceval is_singleton_int : t -> bool

Sourceexception Not_Singleton_Int

Sourceval 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.

Sourceval cardinal : t -> Integer.t option

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

Sourceval 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.

Sourceval cardinal_less_than : t -> int -> int

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

raises Abstract_interp.Not_less_than
is the cardinal of t is more than n

Sourceval cardinal_is_less_than : t -> int -> bool

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

Sourceval 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.

Sourceval 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.

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

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

Sourceval 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).

Sourceval apply_set : (Integer.t -> Integer.t -> Integer.t) -> t -> t -> t

Sourceval apply_set_unary : (Integer.t -> Integer.t) -> t -> t

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

Subdivisions into two intervals

Sourceval 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.

Sourceval 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.

Sourceval 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.

Sourceval 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.

Sourceval 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.

Sourceval div : t -> t -> t

Integer division

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

Integer division

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.

Sourceval c_rem : t -> t -> t

Sourceval mul : t -> t -> t

Sourceval shift_left : t -> t -> t

Sourceval shift_right : t -> t -> t

Sourceval interp_boolean : contains_zero:bool -> contains_non_zero:bool -> t

Source

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.

Sourceval create_all_values_modu : modu:Integer.t -> signed:bool -> size:int -> t

Sourceval create_all_values : signed:bool -> size:int -> t

Sourceval all_values : size:Integer.t -> t -> bool

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

Sourceval backward_mult_int_left : right:t -> result:t -> t option Bottom.or_bottom

Sourceval 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

Source

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

Source

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.

Source

val forward_comp_int : 
  Abstract_interp.Comp.t ->
  t ->
  t ->
  Abstract_interp.Comp.result

Sourceval of_int : int -> t

Sourceval of_int64 : int64 -> t

Casts

Sourceval cast_int_to_int : size:Integer.t -> signed:bool -> t -> t

Sourceval cast_int_to_float : Fval.kind -> t -> t

Sourceval 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.

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

Cast the given float to the given size.

Sourceval cast_float_to_int_inverse : single_precision:bool -> t -> t

floating-point

Sourceval cast_int_to_float_inverse : single_precision:bool -> t -> t

floating-point

integer

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

Sourceval 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).

Sourceval pretty_debug : Format.formatter -> t -> unit

Sourceval get_small_cardinal : unit -> int

Value of option -ilevel

Sourceval intersects : t -> t -> bool

Install

dune-project
Dependency

Authors

Maintainers

Sources

doc/codex.framac_ival/Framac_ival/Ival/index.html

Module `Framac_ival.Ival`Source

General guidelines of this module

package codex

Install

dune-project Dependency

Authors

Maintainers

Sources

doc/codex.framac_ival/Framac_ival/Ival/index.html

Module Framac_ival.IvalSource

General guidelines of this module

dune-project
Dependency

Module `Framac_ival.Ival`Source