package frama-c

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

Integer values abstractions: an abstraction represents a set of integers. Provided with a lattice structure and over-approximations of arithmetic operations.

include Datatype.S_with_collections
include Datatype.S
include Datatype.S_no_copy
include Datatype.Ty
type 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
module Widen_Hints = Datatype.Integer.Set
type size_widen_hint = Integer.t
type generic_widen_hint = Widen_Hints.t
include Eva_lattice_type.Full_AI_Lattice_with_cardinality with type t := t and type widen_hint = size_widen_hint * generic_widen_hint
include Eva_lattice_type.AI_Lattice_with_cardinal_one with type t := t with type widen_hint = size_widen_hint * generic_widen_hint
include Eva_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 : Stdlib.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?

include Eva_lattice_type.With_Top with type t := t
val top : t

largest element

include Eva_lattice_type.With_Widening with type t := t with type widen_hint = size_widen_hint * generic_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 Eva_lattice_type.With_Cardinal_One with type t := t
include Eva_lattice_type.With_Narrow with type t := t
val narrow : t -> t -> t Lattice_bounds.or_bottom

over-approximation of intersection

include Eva_lattice_type.With_Under_Approximation with type t := t

under-approximation of union

val meet : t -> t -> t Lattice_bounds.or_bottom

under-approximation of intersection

include Eva_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 Eva_lattice_type.With_Diff with type t := t
val diff : t -> t -> t Lattice_bounds.or_bottom

diff t1 t2 is an over-approximation of t1-t2. t2 must be an under-approximation or exact.

include Eva_lattice_type.With_Diff_One with type t := t
val diff_if_one : t -> t -> t Lattice_bounds.or_bottom

diff_if_one t1 t2 is an over-approximation of t1-t2.

  • returns

    t1 if t2 is not a singleton.

include Eva_lattice_type.With_Enumeration with type t := t
val fold_enum : (t -> 'a -> 'a) -> t -> 'a -> 'a

Fold on the elements of the value one by one if possible. Raises Abstract_interp.Not_less_than when there is an infinite number of elements to enumerate.

val zero : t
val one : t
val minus_one : t
val zero_or_one : t
val positive_integers : t

All positive integers, including 0.

val negative_integers : t

All negative integers, including 0.

Building.

val inject_singleton : Integer.t -> t

Returns an exact abstraction of the given integer.

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

inject_range min max returns an abstraction of all integers between min and max included. None means that the abstraction is unbounded.

val inject_interval : min:Integer.t option -> max:Integer.t option -> rem:Integer.t -> modu:Integer.t -> t

Builds an abstraction of all integers between min and max included and congruent to rem modulo modu. For min and max, None is the corresponding infinity. Checks that min <= max, modu > 0 and 0 <= rest < modu, and fails otherwise. If possible, reduces min and max according to the modulo.

val make : min:Integer.t option -> max:Integer.t option -> rem:Integer.t -> modu:Integer.t -> t

As inject_interval, but also checks that min and max are congruent to rem modulo modu.

Accessors.

val min_int : t -> Integer.t option

Returns the smallest integer represented by an abstraction. Returns None if it does not exist, i.e. if the abstraction is unbounded.

val max_int : t -> Integer.t option

Returns the highest integer represented by an abstraction. Returns None if it does not exist, i.e. if the abstraction is unbouded.

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

Returns the smallest and highest integers represented by an abstraction.

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

Returns min, max, rem, modu such that for all integers i represented by the given abstraction, i satisfies min ≤ i ≤ max and i ≅ rem modu.

exception Not_Singleton
val project_int : t -> Integer.t

Projects a singleton abstraction into an integer.

val is_small_set : t -> bool

Is an abstraction internally represented as a small integer set?

val project_small_set : t -> Integer.t list option

Cardinality.

val is_singleton : t -> bool
val cardinal_zero_or_one : t -> bool
val cardinal : t -> Integer.t option
val cardinal_estimate : size:Integer.t -> t -> Integer.t
val cardinal_less_than : t -> int -> int
val cardinal_is_less_than : t -> int -> bool
val is_zero : t -> bool
val contains_zero : t -> bool
val contains_non_zero : t -> bool

Arithmetics.

val add : t -> t -> t

Addition of two integer abstractions.

val add_under : t -> t -> t Lattice_bounds.or_bottom

Under-approximation of the addition of two integer abstractions

val add_singleton : Integer.t -> t -> t

Addition of an integer abstraction with a singleton integer. Exact operation.

val neg : t -> t

Negation of an integer abstraction.

val abs : t -> t

Absolute value of an integer abstraction.

val scale : Integer.t -> t -> t

scale f v returns an abstraction of the integers f * x for all x in v. This operation is exact.

val scale_div : pos:bool -> Integer.t -> t -> t

scale_div f v is an over-approximation of the elements x / f for all elements x in v. Uses the computer division (like in C99) if pos is false, and the euclidean division if pos is true.

val scale_div_under : pos:bool -> Integer.t -> t -> t Lattice_bounds.or_bottom

Under-approximation of the division.

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

Over-approximation of the remainder of the division. Uses the computer division (like in C99) if pos is false, and the euclidean division if pos is true.

val mul : t -> t -> t
val div : t -> t -> t Lattice_bounds.or_bottom
val c_rem : t -> t -> t Lattice_bounds.or_bottom
val shift_left : t -> t -> t Lattice_bounds.or_bottom
val shift_right : t -> t -> t Lattice_bounds.or_bottom
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

Comparisons

forward_comp op l r returns the result of the comparison l op r.

val backward_comp_left : Abstract_interp.Comp.t -> t -> t -> t Lattice_bounds.or_bottom

backward_comp_left op l r reduces l by assuming l op r holds.

Misc

val cast_int_to_int : size:Integer.t -> signed:bool -> t -> t
val subdivide : t -> t * t

Splits an abstraction into two abstractions.

val extract_bits : start:Integer.t -> stop:Integer.t -> t -> t

Extracts bits from start to stop from the given integer abstraction, start and stop being included.

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

Builds an abstraction of all integers in a C integer type.

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

val fold_int : ?increasing:bool -> (Integer.t -> 'a -> 'a) -> t -> 'a -> 'a

Iterates on all integers represented by an abstraction, in increasing order by default. If increasing is set to false, iterate by decreasing order.

val to_seq : ?increasing:bool -> t -> Integer.t Stdlib.Seq.t

Builds a sequence of all integers represented by an abstraction, in increasing order (resp. decreasing order if increasing is set to false). The sequence might be infinite.

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