package codex

  1. Overview
  2. Docs
package codex
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Framac_ival.Ival_noinfSource

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

Sourcetype t = private
  1. | Set of Abstract_interp.Int.t array
  2. | 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)

    *)
  3. | Top of Abstract_interp.Int.t * Abstract_interp.Int.t * 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 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

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

Sourceval max_int : t -> Integer.t

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

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

Sourceval min_and_max : t -> Integer.t * Integer.t

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

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 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 -> Integer.t -> t

None means unbounded. The interval is inclusive.

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.

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

Sourceval backward_comp_float_left_true : Abstract_interp.Comp.t -> Fval.kind -> t -> t -> t
Sourceval 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.

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