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.types/Types/TypedC/index.html

Module Types.TypedCSource

TypedC: Grammar for describing the types for the type-based domain, and operations on concrete types.

Sourcetype value_symbol = string
Sourcetype value =
  1. | Sym of value_symbol
Sourcetype array_length =
  1. | Fixed_length of Z.t
  2. | Variable_length of value_symbol
Sourceval pp_value : Format.formatter -> value -> unit
Sourceval pp_array_length : Format.formatter -> array_length -> unit
Sourcemodule Pred : sig ... end
Sourcetype basic = Units.In_bytes.t * string
Sourcetype structure = {
  1. st_byte_size : Units.In_bytes.t;
  2. st_members : (Units.In_bytes.t * string * typ) list;
}
Sourceand union = {
  1. un_byte_size : Units.In_bytes.t option;
  2. un_types : (string * typ) list;
}
Sourceand descr =
  1. | Void
  2. | Base of basic
    (*

    Base types. Note that even if they have a name, they are not a definition (e.g., you cannot have pointers to byte.

    *)
  3. | Structure of structure
  4. | StructureFAM of {
    1. structure : typ;
    2. array : typ;
    }
    (*

    Structure with flexible array member, decomposed as fix prefix * array.

    *)
  5. | Ptr of pointer
    (*

    Todo: we should always have a size (possibly an existentially-qualified variable).

    *)
  6. | Array of typ * array_length
    (*

    Arguments: element type, and the number of elements, if statically known.

    *)
  7. | Function of funtyp
  8. | Application of name
    (*

    ∃ bound_var : bound_typ, inner

    *)
  9. | Existential of {
    1. bound_var : string;
    2. bound_typ : typ;
    3. body : typ;
    }
  10. | Union of union
  11. | Weak of typ
Sourceand pointer = {
  1. pointed : typ;
}
Sourceand name = {
  1. constr : constr;
  2. args : Pred.expr list;
}
Sourceand constr_name =
  1. | ConstrName of string
  2. | ConstrNameFunc of string
  3. | ConstrNameUnion of string
  4. | ConstrNameStruct of string
  5. | ConstrNameEnum of string
  6. | ConstrNameArray of constr_name

Called type name in OOPSLA, but is the name of a family of region names when there are arguments.

Sourceand constr = private {
  1. id : int;
  2. name : constr_name;
  3. arity : int;
}

Each constr_name is associated to a unique id and arity to give a constr.

Sourceand funtyp = {
  1. ret : typ;
  2. args : typ list;
  3. pure : bool;
}
Sourceand typ = {
  1. mutable descr : descr;
  2. mutable pred : Pred.t;
}
Sourcetype fundef = {
  1. funtyp : typ;
  2. inline : bool;
}
Sourceval pp : Format.formatter -> typ -> unit
Sourceval pp_constr : Format.formatter -> constr -> unit
Sourceval compare : typ -> typ -> int
Sourceval equal : typ -> typ -> bool
Sourceval equiv : typ -> typ -> bool

equiv a b returns true if it can show that a is a subtype of b and b is a subtype a.

Sourcemodule Constr : sig ... end
Sourcemodule Build : sig ... end
Sourceval is_flexible_array : typ -> bool
Sourceval is_function_pure : typ -> bool
Sourceval contains : typ -> typ -> bool

contains t u determines whether t contains u. (Definition: t contains u iff t = u or a component of t (e.g. a structure member) contains u.

Sourceexception Unsizeable_type
Sourceval sizeof : typ -> Units.In_bytes.t

Returns the size of the type (in bytes), if possible

Sourceexception Undefined_type_constructor of string

These functions allow to update or query the binding from type names to types.

Sourceval get_type_definitions : unit -> string list
Sourceval inlined : typ -> typ

Unroll the definitions of a type (i.e. replace a name with the corresponding type)

Sourceval substitute_in_type : typ -> (value_symbol * Pred.expr) list -> typ

Substitutes the symbolic variables in the type typ by the corresponding expressions in bindings

Sourceval substitute_symbol : typ -> string -> string -> typ
Sourceval word : byte_size:Units.In_bytes.t -> typ
Sourceval tuple : typ list -> typ

Additionnal functions used for type domains

Sourcetype constr_def = typ * string list
Sourceval add_constr_definition : constr -> constr_def -> unit

Maps a name to a type constructor.

Sourceval constr_of_name : constr -> constr_def option

find the constr_def associated to a constr, or None if none.

Sourceval print_constr_map : Format.formatter -> unit -> unit

print the constructor map, for debug purposes.

Sourceval print_spec : Format.formatter -> unit -> unit

print all the stored maps, for debug purposes

Sourceval add_function_name_definition : string -> typ -> bool -> unit
Sourceval function_of_name : string -> typ option

Retrieve the type associated to a function name, or None if there is none.

Sourceval function_definition_of_name : string -> fundef option

Retrieve the type associated to a function name, and whether it was declared inline; or None if not found.

Sourceval print_function_map : Format.formatter -> unit -> unit

print the function map, for debug purposes.

Sourceval get_function_names : unit -> string list
Sourceval add_global_name_definition : string -> typ -> unit
Sourceval global_of_name : string -> typ option

Retrieve the type associated to a function name, or None if not found.

Sourceval print_global_map : Format.formatter -> unit -> unit

print the function map, for debug purposes.