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.domains/Domains/Memory_domains/Region_suffix_tree/MakeOffset/index.html

Module Region_suffix_tree.MakeOffset

Parameters

module Scalar : Sig.BASE

Signature

include Memory_sig.OFFSET with module Scalar = Scalar with type boolean = Scalar.boolean
include Memory_sig.AADT with module Scalar = Scalar
module Scalar = Scalar
include Memory_sig.WITH_OFFSET with module Scalar := Scalar and type boolean = Scalar.boolean with type boolean = Scalar.boolean
type boolean = Scalar.boolean
type offset
module Offset : sig ... end
val offset_pretty : Scalar.Context.t -> Format.formatter -> offset -> unit
val offset_empty : Scalar.Context.t -> offset
val serialize_offset : widens:bool -> Scalar.Context.t -> offset -> Scalar.Context.t -> offset -> 'a Scalar.Context.in_acc -> (offset, 'a) Scalar.Context.result

Transfer functions

val offset_zero : max:int option -> Scalar.Context.t -> offset

Beginning of a region (offset 0) of size max (in bytes, if known and/or useful).

val offset_shift : offset:int -> max:int option -> Scalar.Context.t -> offset -> offset

offset_shift offset:k o adds a suffix .f, i.e. returns o.f when the field f has relative offset k.

val offset_index : int -> Scalar.Context.t -> offset -> Scalar.binary -> offset

offset_index size:k o i adds a suffix [i], i.e. returns o[i] when o was pointing to an array of elements of size k.

val offset_sub : Scalar.Context.t -> offset -> offset -> Scalar.binary

offset_sub o1 o2 when o1 is a suffix of o2 returns the suffix part. E.g. offset_sub o1.k.a[3] o1 returns .k.a[3].

val offset_le : Scalar.Context.t -> offset -> offset -> boolean

Offset comparison.

val offset_eq : Scalar.Context.t -> offset -> offset -> boolean
val offset_within_bounds : size:Units.In_bits.t -> Scalar.Context.t -> offset -> boolean

Check that all array indices operation are within bound.

val offset_choose : Operator.Choice.t -> Scalar.Context.t -> offset -> offset
val boolean2scalar_bool : Scalar.Context.t -> boolean -> Scalar.boolean

Lift/unlift a boolean to a Scalar.boolean. Probably this should not be part of the domain signature.

val scalar_bool2boolean : Scalar.Context.t -> Scalar.boolean -> boolean
val fold_crop : size:Units.In_bits.t -> Scalar.Context.t -> offset -> inf:Z.t -> sup:Z.t -> (Z.t -> 'a -> 'a) -> 'a -> 'a
val in_bounds : size:Units.In_bits.t -> Scalar.Context.t -> offset -> inf:Z.t -> sup:Z.t -> bool