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/Abstract_interp/Int/index.html

Module Abstract_interp.IntSource

include module type of Integer with type t = Z.t
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 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".

Sourcemodule Set : sig ... end
Sourceval pretty : Format.formatter -> t -> unit
Sourceval 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