Frama-C:
Plug-ins:
Libraries:

Frama-C API - Int

include module type of Integer with type t = Integer.t
type 'a formatter = Stdlib.Format.formatter -> 'a -> unit
type t = Integer.t
val le : t -> t -> bool
val ge : t -> t -> bool
val lt : t -> t -> bool
val gt : t -> t -> bool
val add : t -> t -> t
val sub : t -> t -> t
val mul : t -> t -> t
val shift_left : t -> t -> t
  • raises Invalid_argument

    if second argument (count) is negative

val shift_right : t -> t -> t
  • raises Invalid_argument

    if second argument (count) is negative

val shift_right_logical : t -> t -> t
  • raises Invalid_argument

    if any argument is negative

val logand : t -> t -> t
val logor : t -> t -> t
val logxor : t -> t -> t
val lognot : t -> t
val min : t -> t -> t
val max : t -> t -> t
val e_div : t -> t -> t

Euclidean division (that returns a positive rem). Implemented by Z.ediv

Equivalent to C division if both operands are positive. Equivalent to a floored division if b > 0 (rounds downwards), otherwise rounds upwards. Note: it is possible that e_div (-a) b <> e_div a (-b).

val e_rem : t -> t -> t

Remainder of the Euclidean division (always positive). Implemented by Z.erem

val e_div_rem : t -> t -> t * t

e_div_rem a b returns (e_div a b, e_rem a b). Implemented by Z.ediv_rem

val c_div : t -> t -> t

Truncated division towards 0 (like in C99). Implemented by Z.div

val c_rem : t -> t -> t

Remainder of the truncated division towards 0 (like in C99). Implemented by Z.rem

val c_div_rem : t -> t -> t * t

c_div_rem a b returns (c_div a b, c_rem a b). Implemented by Z.div_rem

val pgcd : t -> t -> t

pgcd v 0 == pgcd 0 v == abs v. Result is always positive

val ppcm : t -> t -> t

ppcm v 0 == ppcm 0 v == 0. Result is always positive

val cast : size:t -> signed:bool -> value:t -> t
val abs : t -> t
val neg : t -> t
val succ : t -> t
val pred : t -> t
val is_zero : t -> bool
val is_one : t -> bool
val is_even : t -> bool
val zero : t
val one : t
val two : t
val four : t
val eight : t
val sixteen : t
val thirtytwo : t
val onethousand : t
val billion_one : t
val minus_one : t
val max_int64 : t
val min_int64 : t
val two_power_32 : t
val two_power_64 : t
val length : t -> t -> t

b - a + 1

val of_int : int -> t
val of_int64 : Stdlib.Int64.t -> t
val of_int32 : Stdlib.Int32.t -> t
val to_int_exn : t -> int
  • raises Z.Overflow

    if too big

  • since 24.0-Chromium
val to_int64_exn : t -> int64
  • raises Z.Overflow

    if too big

  • since 24.0-Chromium
val to_int32_exn : t -> int32
  • raises Z.Overflow

    if too big

  • since 24.0-Chromium
val to_int_opt : t -> int option

Returns Some i if the number can be converted to an int, or None otherwise.

  • since 24.0-Chromium
val to_int64_opt : t -> int64 option

Returns Some i if the number can be converted to an int64, or None otherwise.

  • since 24.0-Chromium
val to_int32_opt : t -> int32 option

Returns Some i if the number can be converted to an int32, or None otherwise.

  • since 24.0-Chromium
val to_float : t -> float
val of_float : float -> t
val round_up_to_r : min:t -> r:t -> modu:t -> t

round_up_to_r m r modu is the smallest number n such that n>=m and n = r modulo modu

val round_down_to_r : max:t -> r:t -> modu:t -> t

round_down_to_r m r modu is the largest number n such that n<=m and n = r modulo modu

val two_power : t -> t

Computes 2^n

  • raises Z.Overflow

    for exponents greater than 1024

val two_power_of_int : int -> t

Computes 2^n

val power_int_positive_int_opt : int -> int -> t option

Exponentiation

val extract_bits : start:t -> stop:t -> t -> t
val popcount : t -> int
val to_string : t -> string
val of_string : string -> t
  • raises Invalid_argument

    when the string cannot be parsed.

val pretty_hex : t formatter

Prints the integer in hexadecimal format (replaces hexa optional argument of pretty from older versions).

  • since 25.0-Manganese
val pp_bin : ?nbits:int -> ?sep:string -> t formatter

Print binary format. Digits are output by blocs of 4 bits separated by ~sep with at least ~nbits total bits. If nbits is non positive, it will be ignored.

Positive values are prefixed with "0b" and negative values are printed as their 2-complement (lnot) with prefix "1b".

val pp_hex : ?nbits:int -> ?sep:string -> t formatter

Print hexadecimal format. Digits are output by blocs of 16 bits (4 hex digits) separated by ~sep with at least ~nbits total bits. If nbits is non positive, it will be ignored.

Positive values are preffixed with "0x" and negative values are printed as their 2-complement (lnot) with prefix "1x".

include Lattice_type.Lattice_Value 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
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 fold : (t -> 'a -> 'a) -> inf:t -> sup:t -> step:t -> 'a -> 'a

Fold the function on the value between inf and sup at every step. If step is positive the first value is inf and values go increasing, if step is negative the first value is sup and values go decreasing