package goblint-cil

  1. Overview
  2. Docs
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module GoblintCil.CilintSource

The cilint type is public and not just big_int to make life with ocamldebug easier. Please do not rely on this representation, use the ..._of_cilint functions to get at a cilint's value.

Sourceval zero_cilint : cilint

0 as a cilint

Sourceval one_cilint : cilint

1 as a cilint

Sourceval mone_cilint : cilint

-1 as a cilint

Sourcetype truncation =
  1. | NoTruncation
  2. | ValueTruncation
  3. | BitTruncation

Result type for truncate_... functions

Sourceval truncate_signed_cilint : cilint -> int -> cilint * truncation

Truncate a cilint to an n-bit, signed 2's complement integer. Returns the truncated value, and an indication of the loss of precision. NoTruncation means the truncated value = original value. ValueTruncation means that truncated value <> original value, but the original value was between -2^(n-1) and (2^n)-1, so no "interesting" (not all-0 or all-1) bits were lost. If neither condition holds, the result is BitTruncation.

Sourceval truncate_unsigned_cilint : cilint -> int -> cilint * truncation

Truncate a cilint to an n-bit, unsigned integer. Returns the truncated value, and an indication of the loss of precision. NoTruncation means the truncated value = original value. ValueTruncation means that truncated value <> original value, but the original value was between -2^(n-1) and (2^n)-1, so no "interesting" (not all-0 or all-1) bits were lost. If neither condition holds, the result is BitTruncation.

Sourceval neg_cilint : cilint -> cilint

Negate a cilint

Sourceval add_cilint : cilint -> cilint -> cilint

Add two cilints

Sourceval sub_cilint : cilint -> cilint -> cilint

Subtract two cilints

Sourceval mul_cilint : cilint -> cilint -> cilint

Multiply two cilints

Sourceval div_cilint : cilint -> cilint -> cilint

Divide two cilints, rounding down

Sourceval mod_cilint : cilint -> cilint -> cilint

Remainder for div_cilint

Sourceval div0_cilint : cilint -> cilint -> cilint

Divide two cilints, rounding towards zero

Sourceval rem_cilint : cilint -> cilint -> cilint

Remainder for div0_cilint

Sourceval lognot_cilint : cilint -> cilint

Bitwise-not a cilint

Sourceval logand_cilint : cilint -> cilint -> cilint

Bitwise-and of two cilints

Sourceval logor_cilint : cilint -> cilint -> cilint

Bitwise-or of two cilints

Sourceval logxor_cilint : cilint -> cilint -> cilint

Bitwise-xor of two cilints

Sourceval shift_left_cilint : cilint -> int -> cilint

Left-shift a cilint

Sourceval shift_right_cilint : cilint -> int -> cilint

Right-shift a cilint. Note that there's no shift_right_logical_cilint as that makes no sense on an infinite precision 2's complement integer

Sourceval int_of_cilint : cilint -> int

Return the cilint's value as an integer, or raise Failure if the value doesn't fit in an int

Sourceval int64_of_cilint : cilint -> int64

Return the low-order 64-bits of cilint's value as an int64. Note that this never fails.

Sourceval big_int_of_cilint : cilint -> Big_int_Z.big_int

Return the cilint's value as a big_int

Sourceval string_of_cilint : cilint -> string

Return the cilint's value as a string

Sourceval cilint_of_int : int -> cilint

Make a cilint from an int

Sourceval cilint_of_int64 : int64 -> cilint

Make a cilint from an int64

Sourceval cilint_of_big_int : Big_int_Z.big_int -> cilint

Make a cilint from a big_int

Sourceval cilint_of_string : string -> cilint

Make a cilint from a string

Sourceval is_zero_cilint : cilint -> bool

Return true if the cilint is 0

Sourceval compare_cilint : cilint -> cilint -> int

ordering function for two cilints

Sourceval is_int_cilint : cilint -> bool

Return true if the cilint's value is representable in an int

OCaml

Innovation. Community. Security.