package frama-c

  1. Overview
  2. Docs
package frama-c
Legend:
Library
Module
Module type
Parameter
Class
Class type

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.
module Widen_Hints = Datatype.Integer.Set
type size_widen_hint = Integer.t
type numerical_widen_hint = Widen_Hints.t * Fc_float.Widen_Hints.t
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 and type widen_hint = size_widen_hint * numerical_widen_hint
include Lattice_type.AI_Lattice_with_cardinal_one with type t := t with type widen_hint = size_widen_hint * numerical_widen_hint
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 : 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_Widening with type t := t with type widen_hint = size_widen_hint * numerical_widen_hint

hints for the widening

val widen : widen_hint -> t -> t -> t

widen h t1 t2 is an over-approximation of join t1 t2. Assumes is_included t1 t2

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

val pretty_debug : Format.formatter -> t -> unit
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct