package codex

You can search for identifiers within the package.

in-package search v0.2.0

The Codex library for building static analysers based on abstract interpretation

Install

dune-project

Dependency

codex.top Edit opam file Versions (1)

Authors

Maintainers

M

Matthieu Lemerre <matthieu.lemerre@cea.fr>

Sources

1.0-rc4.tar.gz

md5=bc7266a140c6886add673ede90e335d3

sha512=8da42c0ff2c1098c5f9cb2b5b43b306faf7ac93b8f5ae00c176918cee761f249ff45b29309f31a05bbcf6312304f86a0d5a000eb3f1094d3d3c2b9b4c7f5c386

doc/codex.domains/Domains/Overflow_checks/Make/argument-1-Sub/Integer_Forward/index.html

Module `Sub.Integer_Forward`

val itimes : Z.t -> (integer, integer) Sig.Context_Arity_Forward(Context).ar1

Multiply an integer by a constant

val iadd : (integer, integer, integer) Sig.Context_Arity_Forward(Context).ar2

val imul : (integer, integer, integer) Sig.Context_Arity_Forward(Context).ar2

val idiv : (integer, integer, integer) Sig.Context_Arity_Forward(Context).ar2

This is truncated (C99-like) integer division

val imod : (integer, integer, integer) Sig.Context_Arity_Forward(Context).ar2

val ishl : (integer, integer, integer) Sig.Context_Arity_Forward(Context).ar2

val ishr : (integer, integer, integer) Sig.Context_Arity_Forward(Context).ar2

val iand : (integer, integer, integer) Sig.Context_Arity_Forward(Context).ar2

Bitwise and, where negative integers are seen as prefixed by infinite ones

val ior : (integer, integer, integer) Sig.Context_Arity_Forward(Context).ar2

Bitwise or, where negative integers are seen as prefixed by infinite ones

val ixor : (integer, integer, integer) Sig.Context_Arity_Forward(Context).ar2

val isub : (integer, integer, integer) Sig.Context_Arity_Forward(Context).ar2

val ieq : (integer, integer, boolean) Sig.Context_Arity_Forward(Context).ar2

val ile : (integer, integer, boolean) Sig.Context_Arity_Forward(Context).ar2

val iconst : Z.t -> integer Sig.Context_Arity_Forward(Context).ar0

Integer constant

val zero : integer Sig.Context_Arity_Forward(Context).ar0

These can be defined from the others, but it may be more efficient to implement them directly (no need to build temporary values...). They are also often convenient to use directly.

val one : integer Sig.Context_Arity_Forward(Context).ar0