package frama-c

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

Small sets of integers.

Above a certain limit fixed by set_small_cardinal, these sets must be converted into intervals. The functions that make the set grow returns a set_or_top type : either the resulting sets is small enough, or it is converted into an interval.

Sets are always non-empty. The functions reducing the sets returns a set or_bottom type: either the result is non-empty, or it is `Bottom.

val get_small_cardinal : unit -> int

Returns the limit above which integer sets are converted into intervals.

val set_small_cardinal : int -> unit

Sets the limit above which integer sets are converted into intervals. This is used by the Eva plugin according to the -eva-ilevel option. Do not use.

include Datatype.S_with_collections
include Datatype.S
include Datatype.S_no_copy
include Datatype.Ty
type 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.

module Set : Datatype.Set with type elt = t
module Map : Datatype.Map with type key = t
module Hashtbl : Datatype.Hashtbl with type key = t
val inject_singleton : Integer.t -> t

Creates the set containing only the given integer.

val inject_periodic : from:Integer.t -> period:Integer.t -> number:Integer.t -> t

Creates the set with integers from + k*period for k in {0 ... number-1}. The resulting set contains number integers. There is no verification about number, but it should be stritly positive.

val inject_list : Integer.t list -> t

Creates a set from an integer list. The list must not be empty, and the list length must not exceed the small cardinal limit.

val to_list : t -> Integer.t list

Returns the set as an integer list.

Removes an integer from a set. Returns Bottom if the resulting set is empty.

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

mem i s is true iff the set s contains the integer i.

val one : t
val zero : t
val minus_one : t
val zero_or_one : t
val min : t -> Integer.t

Returns the smallest integer of a set.

val max : t -> Integer.t

Returns the highest integer of a set.

val cardinal : t -> int

Returns the number of integers in a set.

Iterators on the integers of a set.

val for_all : (Integer.t -> bool) -> t -> bool
val exists : (Integer.t -> bool) -> t -> bool
val iter : (Integer.t -> unit) -> t -> unit
val fold : ?increasing:bool -> (Integer.t -> 'a -> 'a) -> t -> 'a -> 'a
val map : (Integer.t -> Integer.t) -> t -> t
val filter : (Integer.t -> bool) -> t -> t Lattice_bounds.or_bottom
val map_reduce : (Integer.t -> 'a) -> ('a -> 'a -> 'a) -> t -> 'a
val to_seq : ?increasing:bool -> t -> Integer.t Stdlib.Seq.t
type set_or_top = [
  1. | `Set of t
    (*

    Small set.

    *)
  2. | `Top of Integer.t * Integer.t * Integer.t
    (*

    Interval: min, max, modu

    *)
]

Sets whose cardinal exceeds a certain limit must be converted into intervals. Functions that make sets grow returns either a set small enough, or the information needed to construct the corresponding interval: the smallest and highest elements, and the periodicity of the integers of the set.

type set_or_top_or_bottom = [
  1. | `Bottom
  2. | set_or_top
]
val apply2 : (Integer.t -> Integer.t -> Integer.t) -> t -> t -> set_or_top

apply2 f s1 s2 applies f i1 i2 for all integers i1 in s1 and i2 in s2.

Lattice structure.

val is_included : t -> t -> bool
val join : t -> t -> set_or_top
val meet : t -> t -> t Lattice_bounds.or_bottom
val narrow : t -> t -> t Lattice_bounds.or_bottom
val intersects : t -> t -> bool
val diff_if_one : t -> t -> t Lattice_bounds.or_bottom
val complement_under : min:Integer.t -> max:Integer.t -> t -> set_or_top_or_bottom

Semantics.

See Int_val for more details.

val add_singleton : Integer.t -> t -> t
val add : t -> t -> set_or_top
val add_under : t -> t -> set_or_top
val neg : t -> t
val abs : t -> t
val mul : t -> t -> set_or_top
val c_rem : t -> t -> set_or_top_or_bottom
val scale : Integer.t -> t -> t
val scale_div : pos:bool -> Integer.t -> t -> t
val scale_rem : pos:bool -> Integer.t -> t -> t
val bitwise_signed_not : t -> t

Misc

val subdivide : t -> t * 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