Frama-C:
Plug-ins:
Libraries:

Frama-C API - Int_set

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