module Ival:sig
..end
Arithmetic lattices. The interfaces of this module may change between Frama-C versions. Contact us if you need stable APIs.
type
t
_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 Ival.is_zero
.Lattice_type
about over- and under-approximations,
and exact operations.module Widen_Hints: Datatype.Integer.Set
typesize_widen_hint =
Integer.t
typenumerical_widen_hint =
Widen_Hints.t * Fc_float.Widen_Hints.t
include Datatype.S_with_collections
include Lattice_type.Full_AI_Lattice_with_cardinality
val is_bottom : t -> bool
val overlaps : partial:bool -> size:Integer.t -> t -> 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.
Abstract_interp.Error_Bottom
if the argument is bottom.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 : t -> Integer.t
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
.
Abstract_interp.Not_less_than
is the cardinal of t
is more than 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_intrep.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 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 Bottom.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 Ival.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 Bottom.or_bottom
Returns an under-approximation of the integers of the given size and signedness that are *not* represented by the given ival.
val pretty_debug : Stdlib.Format.formatter -> t -> unit