package frama-c

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

Integer intervals with congruence. An interval defined by min, max, rem, modu represents all integers between the bounds min and max and congruent to rem modulo modu. A value of None for min (resp. max) represents -infinity (resp. +infinity). modu is > 0, and 0 <= rem < modu.

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
include Eva_lattice_type.Full_AI_Lattice_with_cardinality with type t := t
include Eva_lattice_type.AI_Lattice_with_cardinal_one with type t := t
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 : 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_Cardinal_One with type t := t
val cardinal_zero_or_one : t -> bool
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 cardinal_less_than : t -> int -> int

Raises Abstract_interp.Not_less_than whenever the cardinal of the given lattice is strictly higher than the given integer.

type widen_hint = Datatype.Integer.Set.t

Hints for the widening: set of relevant thresholds.

val widen : ?size:Integer.t -> ?hint:widen_hint -> t -> t -> t

widen ~size ~hint t1 t2 is an over-approximation of join t1 t2. size is the size (in bits) of the widened value, hint is a set of relevant thresholds for the widened interval bounds.

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

Checks that the interval defined by min, max, rem, modu is well formed.

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

Makes the interval of all integers between min and max and congruent to rem modulo modu. Fails if these conditions does not hold:

  • min ≤ max
  • 0 ≤ rem < modu
  • min ≅ rem modu ∧ max ≅ rem modu
val inject_range : Integer.t option -> Integer.t option -> t

Makes the interval of all integers between min and max.

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

Returns the bounds of the given interval. None means infinity.

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

Returns the bounds and the modulo of the given interval.

val mem : Integer.t -> t -> bool

mem i t returns true iff the integer i is in the interval t.

val cardinal : t -> Integer.t option

Returns the number of integers represented by the given interval. Returns None if the interval represents an infinite number of integers.

val complement_under : min:Integer.t -> max:Integer.t -> t -> t Lattice_bounds.or_bottom

Returns an under-approximation of the integers between min and max that are *not* represented by the given interval.

Interval semantics.

See Int_val for more details.

val add_singleton_int : Integer.t -> t -> t
val add : t -> t -> t
val add_under : t -> t -> t Lattice_bounds.or_bottom
val neg : t -> t
val abs : t -> t
val scale : Integer.t -> t -> t
val scale_div : pos:bool -> Integer.t -> t -> t
val scale_div_under : pos:bool -> Integer.t -> t -> t Lattice_bounds.or_bottom
val scale_rem : pos:bool -> Integer.t -> t -> t
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 cast : size:Integer.t -> signed:bool -> t -> t

Misc.

val subdivide : t -> t * t
val reduce_sign : t -> bool -> t Lattice_bounds.or_bottom
val reduce_bit : int -> t -> bool -> t Lattice_bounds.or_bottom
val fold_int : ?increasing:bool -> (Integer.t -> 'a -> 'a) -> t -> 'a -> 'a
val to_seq : ?increasing:bool -> t -> Integer.t Seq.t
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