Frama-C:
Plug-ins:
Libraries:

Frama-C API - Z

Extension of Z from Zarith. Fc_internal_z only includes to Zarith.Z module, it is mandatory if we want to call this module Z without shadowing Zarith's module. This solution is a bit ugly and could be replace by root_module in kernel dune file, but this does not work for now...

  • before Frama-C+dev

    this module was called Integer

Previous version of this file did not include Z, so many more functions and operators are available now.

  • since Frama-C+dev
include module type of Fc_internal_z with type t = Fc_internal_z.t
include module type of Z with type t = Z.t with type t = Fc_internal_z.t
exception Overflow
val zero : t
val one : t
val minus_one : t
val of_int : int -> t
val of_int32 : int32 -> t
val of_int64 : int64 -> t
val of_nativeint : nativeint -> t
val of_int32_unsigned : int32 -> t
val of_int64_unsigned : int64 -> t
val of_nativeint_unsigned : nativeint -> t
val of_float : float -> t
val of_string : string -> t
val of_substring : string -> pos:int -> len:int -> t
val of_string_base : int -> string -> t
val of_substring_base : int -> string -> pos:int -> len:int -> t
val succ : t -> t
val pred : t -> t
val abs : t -> t
val neg : t -> t
val add : t -> t -> t
val sub : t -> t -> t
val mul : t -> t -> t
val div : t -> t -> t
val rem : t -> t -> t
val div_rem : t -> t -> t * t
val cdiv : t -> t -> t
val fdiv : t -> t -> t
val ediv_rem : t -> t -> t * t
val ediv : t -> t -> t
val erem : t -> t -> t
val divexact : t -> t -> t
val divisible : t -> t -> bool
val congruent : t -> t -> t -> bool
val logand : t -> t -> t
val logor : t -> t -> t
val logxor : t -> t -> t
val lognot : t -> t
val shift_left : t -> int -> t
val shift_right : t -> int -> t
val shift_right_trunc : t -> int -> t
val numbits : t -> int
val trailing_zeros : t -> int
val testbit : t -> int -> bool
val popcount : t -> int
val hamdist : t -> t -> int
val to_int : t -> int
val to_int32 : t -> int32
val to_int64 : t -> int64
val to_nativeint : t -> nativeint
val to_int32_unsigned : t -> int32
val to_int64_unsigned : t -> int64
val to_nativeint_unsigned : t -> nativeint
val to_float : t -> float
val to_string : t -> string
val format : string -> t -> string
val fits_int : t -> bool
val fits_int32 : t -> bool
val fits_int64 : t -> bool
val fits_nativeint : t -> bool
val fits_int32_unsigned : t -> bool
val fits_int64_unsigned : t -> bool
val fits_nativeint_unsigned : t -> bool
val print : t -> unit
val output : Stdlib.out_channel -> t -> unit
val sprint : unit -> t -> string
val bprint : Stdlib.Buffer.t -> t -> unit
val pp_print : Stdlib.Format.formatter -> t -> unit
val leq : t -> t -> bool
val geq : t -> t -> bool
val lt : t -> t -> bool
val gt : t -> t -> bool
val sign : t -> int
val min : t -> t -> t
val max : t -> t -> t
val is_even : t -> bool
val is_odd : t -> bool
val seeded_hash : int -> t -> int
val gcd : t -> t -> t
val gcdext : t -> t -> t * t * t
val lcm : t -> t -> t
val powm : t -> t -> t -> t
val powm_sec : t -> t -> t -> t
val invert : t -> t -> t
val probab_prime : t -> int -> int
val nextprime : t -> t
val jacobi : t -> t -> int
val legendre : t -> t -> int
val kronecker : t -> t -> int
val remove : t -> t -> t * int
val fac : int -> t
val fac2 : int -> t
val facM : int -> int -> t
val primorial : int -> t
val bin : t -> int -> t
val fib : int -> t
val lucnum : int -> t
val pow : t -> int -> t
val sqrt : t -> t
val sqrt_rem : t -> t * t
val root : t -> int -> t
val rootrem : t -> int -> t * t
val perfect_power : t -> bool
val perfect_square : t -> bool
val log2 : t -> int
val log2up : t -> int
val size : t -> int
val extract : t -> int -> int -> t
val signed_extract : t -> int -> int -> t
val to_bits : t -> string
val of_bits : string -> t
val random_int : ?rng:Stdlib.Random.State.t -> t -> t
val random_bits : ?rng:Stdlib.Random.State.t -> int -> t
val random_int_gen : fill:(bytes -> int -> int -> unit) -> t -> t
val random_bits_gen : fill:(bytes -> int -> int -> unit) -> int -> t
val (~-) : t -> t
val (~+) : t -> t
val (+) : t -> t -> t
val (-) : t -> t -> t
val (*) : t -> t -> t
val (/) : t -> t -> t
val (/>) : t -> t -> t
val (/<) : t -> t -> t
val (/|) : t -> t -> t
val (mod) : t -> t -> t
val (land) : t -> t -> t
val (lor) : t -> t -> t
val (lxor) : t -> t -> t
val (~!) : t -> t
val (lsl) : t -> int -> t
val (asr) : t -> int -> t
val (~$) : int -> t
val (**) : t -> int -> t
module Compare : sig ... end
val version : string
val round_to_float : t -> bool -> float

Z.t is a Frama-C Datatype, and comes with usual compare, equal, hash and pretty functions.

  • since Frama-C+dev
include Datatype.S_with_collections 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 datatype_name : string

Unique name of the datatype.

val datatype_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 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 integer : t Type.t
  • since Frama-C+dev

Operators

module Operators : sig ... end

This module contains all Z operators.

Compare operators are not at top level in Zarith.

  • since Frama-C+dev
include module type of Compare
val (=) : t -> t -> bool
val (<) : t -> t -> bool
val (>) : t -> t -> bool
val (<=) : t -> t -> bool
val (>=) : t -> t -> bool
val (<>) : t -> t -> bool

Conversions

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_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_int64_opt : t -> int64 option

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

  • since 24.0-Chromium

Basic functions, most of them from Z

val is_zero : t -> bool

Return true if the given argument is equal to zero.

val is_one : t -> bool

Return true if the given argument is equal to one.

val length : t -> t -> t

Compute b - a + 1.

val two_power_of_int : ?limit:int -> int -> t

Computes 2^n. ?limit can be used to raise an Overflow if the exponent is too big. Default value is 1024.

  • raises Overflow

    if the argument is greater than ?limit

  • before Frama-C+dev

    ?limit argument was not present and all values were accepted

val two_power : ?limit:int -> t -> t

Calls two_power_of_int after converting the argument using to_int. The default value of ?limit is set by two_power_of_int.

  • raises Overflow

    if the argument is greater than limit or if the conversion fails

  • before Frama-C+dev

    ?limit argument was not present and fixed at 1024

val shift_left_z : t -> t -> t

Convert the second argument via of_int then call shift_left. This function was previously called shift_left but it was renamed to avoid shadowing Z function.

  • since Frama-C+dev
val shift_right_z : t -> t -> t

Convert the second argument via of_int then call shift_right. This function was previously called shift_right but it was renamed to avoid shadowing Z function.

  • since Frama-C+dev
val shift_right_logical : t -> t -> t
  • raises Invalid_argument

    if any argument is negative

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 extract_bits : start:t -> stop:t -> t -> t

extract_bits ~start ~stop v is a shortcut for extract v pos length where pos and length are computed using start and stop.

val cast : size:t -> signed:bool -> value:t -> t

Printers

val set_big_ints_hex : int -> unit

Set a maximum above which big ints will be printed in hexadecimal. A Negative value turns off this option.

  • since Frama-C+dev
val pretty_hex : t Pretty_utils.formatter

Prints the integer in hexadecimal format.

  • since 25.0-Manganese

Prints the integer in either decimal or hexadecimal depending on the value set via set_big_ints_hex.

  • before 25.0-Manganese

    there was an optional hexa argument.

  • before Frama-C+dev

    Only printed in decimal

val pp_bin : ?nbits:int -> ?sep:string -> t Pretty_utils.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 Pretty_utils.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 prefixed with "0x" and negative values are printed as their 2-complement (lnot) with prefix "1x".