package codex

  1. Overview
  2. Docs
The Codex library for building static analysers based on abstract interpretation

Install 

dune-project
 Dependency

codex.top Edit opam file Versions (1)

Authors

  1. M
    Matthieu Lemerre
  2. J
    Julien Simonnet
  3. O
    Olivier Nicole
  4. P
    Paul Robert
  5. D
    Dorian Lesbre
  6. I
    Iker Canut
  7. C
    Corentin Gendreau
  8. G
    Guillaume Girol
  9. C
    Charles Babu
  10. J
    Jérôme Faucheux

Maintainers

  1. M
    Matthieu Lemerre <matthieu.lemerre@cea.fr>

Sources

1.0-rc4.tar.gz
md5=bc7266a140c6886add673ede90e335d3
sha512=8da42c0ff2c1098c5f9cb2b5b43b306faf7ac93b8f5ae00c176918cee761f249ff45b29309f31a05bbcf6312304f86a0d5a000eb3f1094d3d3c2b9b4c7f5c386

doc/codex.framac_ival/Framac_ival/Integer/index.html

Module Framac_ival.IntegerSource

Extension of Big_int compatible with Zarith.

  • since Nitrogen-20111001
Sourcetype t = Z.t
Sourceval equal : t -> t -> bool
Sourceval compare : t -> t -> int
Sourceval le : t -> t -> bool
Sourceval ge : t -> t -> bool
Sourceval lt : t -> t -> bool
Sourceval gt : t -> t -> bool
Sourceval add : t -> t -> t
Sourceval sub : t -> t -> t
Sourceval mul : t -> t -> t
Sourceval shift_left : t -> t -> t
Sourceval shift_right : t -> t -> t
Sourceval shift_right_logical : t -> t -> t
Sourceval logand : t -> t -> t
Sourceval logor : t -> t -> t
Sourceval logxor : t -> t -> t
Sourceval lognot : t -> t
Sourceval min : t -> t -> t
Sourceval max : t -> t -> t
Sourceval 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).

Sourceval e_rem : t -> t -> t

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

Sourceval 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

Sourceval c_div : t -> t -> t

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

Sourceval c_rem : t -> t -> t

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

Sourceval 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

Sourceval pgcd : t -> t -> t

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

Sourceval ppcm : t -> t -> t

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

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

b - a + 1

Sourceval of_int : int -> t
Sourceval of_int64 : Int64.t -> t
Sourceval of_int32 : Int32.t -> t
Sourceval to_int : t -> int
Sourceval to_int64 : t -> int64
Sourceval to_int32 : t -> int32
Sourceval to_float : t -> float
Sourceval of_float : float -> t
Sourceval 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

Sourceval 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

Sourceval two_power : t -> t

Computes 2^n

Sourceval two_power_of_int : int -> t

Computes 2^n

Sourceval power_int_positive_int : int -> int -> t

Exponentiation

Sourceval extract_bits : start:t -> stop:t -> t -> t
Sourceval popcount : t -> int
Sourceval hash : t -> int
Sourceval to_string : t -> string
Sourceval of_string : string -> t
Sourceval pretty : ?hexa:bool -> t Pretty_utils.formatter
Sourceval 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".

Sourceval 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 preffixed with "0x" and negative values are printed as their 2-complement (lnot) with prefix "1x".