Previous  Up  Next

Module Ival

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 = 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


module Widen_Hints: sig .. end
exception Error_Bottom
type size_widen_hint = Integer.t 
type generic_widen_hint = Widen_Hints.t 
include Datatype.S_with_collections
include Lattice_type.Full_AI_Lattice_with_cardinality
val is_bottom : t -> bool
val partially_overlaps : size:Integer.t -> t -> 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 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
val bitwise_and : size:int -> signed:bool -> t -> t -> t
val bitwise_or : t -> t -> t
val bitwise_xor : t -> t -> t
val bitwise_not : t -> t
val bitwise_not_size : size:int -> signed:bool -> t -> t
bitwise negation on a finite integer type. The argument is assumed to fit within the type.
val min_and_max_float : t -> Fval.F.t * Fval.F.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
val contains_non_zero : t -> bool
val top_float : t
val top_single_precision_float : t
exception Nan_or_infinite
val project_float : t -> Fval.t
Raises Nan_or_infinite when the float may be NaN or infinite.
val force_float : Cil_types.fkind -> t -> bool * t
Reinterpret the given value as a float of the given kind. If the returned boolean is true, some of the values may not be representable as finite floats.

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.
val inject_top : Integer.t option -> Integer.t option -> Integer.t -> Integer.t -> t
Deprecated.Ival.inject_interval offers a better API, and normalizes the min and max bounds.
inject_top min max r m checks min, max, r and m for consistency as arguments of the Top constructor and returns the lattice element of integers equal to r modulo m between min and max (which may be a Set if there are few of these). For min and max, None means unbounded.

Cardinality
val cardinal_zero_or_one : t -> bool
val is_singleton_int : t -> bool
exception Not_Singleton_Int
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 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 -> 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.
Raises 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 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 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 Error_Top if the argument is a non-singleton float or a potentially infinite integer.
val fold_split : split:int -> (t -> 'a -> 'a) -> t -> 'a -> 'a
val apply_set : (Integer.t -> Integer.t -> Integer.t) -> t -> t -> t
val apply_set_unary : (Integer.t -> Integer.t) -> t -> t
val subdiv_float_interval : size:int -> t -> t * t
val subdiv_int : t -> t * t
val compare_min_float : t -> t -> int
compare_min_float m1 m2 returns 1 if the float interval m1 has a better min bound (i.e. greater) than the float interval m2.

compare_max_float m1 m2 returns 1 if the float interval m1 has a better max bound (i.e. lower) than the float interval m2.

val compare_max_float : t -> t -> int
compare_min_int m1 m2 returns 1 if the int interval m1 has a better min bound (i.e. greater) than the int interval m2.
val compare_min_int : t -> t -> int
compare_max_int m1 m2 returns 1 if the int interval m1 has a better max bound (i.e. lower) than the int interval m2.
val compare_max_int : t -> t -> int
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 / f for x in v.

scale_div ~pos:true f v is an over-approximation of the set of elements x pos_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 / f for x in v.

scale_div_under ~pos:true f v is an under-approximation of the set of elements x pos_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 mod f for x in v.

scale_rem ~pos:true f v is an over-approximation of the set of elements x pos_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_modu : modu:Integer.t -> signed:bool -> size:int -> t
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_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 : Abstract_interp.Comp.t ->
       bool -> Fval.float_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 compare_max_min : Integer.t option -> Integer.t option -> int
In the results of min_int and max_int, None represents the corresponding infinity. compare_max_min ma mi compares ma to mi, interpreting None for ma as +infinity and None for mi as -infinity.

In the results of min_int and max_int, None represents the corresponding infinity. compare_min_max mi ma compares ma to ma, interpreting None for ma as +infinity and None for mi as -infinity.

val compare_min_max : Integer.t option -> Integer.t option -> int
val scale_int_base : Int_Base.t -> t -> t
val cast_float_to_int : signed:bool -> size:int -> t -> bool * (bool * bool) * t
val cast_float_to_int_inverse : single_precision:bool -> t -> t
integer
val cast_int_to_float_inverse : single_precision:bool -> t -> t
integer
val of_int : int -> t
val of_int64 : int64 -> t
val cast_int_to_float : Fval.rounding_mode -> t -> bool * t
val cast : size:Integer.t -> signed:bool -> value:t -> t
val cast_float : rounding_mode:Fval.rounding_mode -> t -> bool * t
val cast_double : t -> bool * t
val pretty_debug : Format.formatter -> t -> unit
val get_small_cardinal : unit -> int
Value of option -ilevel