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.while_ast/While_ast/index.html

Module While_astSource

Abstract syntax for the while language

Sourcemodule Var : sig ... end

For referring to named storage locations, we use the Var module which ensures that each variable of type t is a record with name and a unique internal identifier to prevent any clashes.

Sourcetype aexp =
  1. | Int of int
    (*

    integer constant

    *)
  2. | Var of Var.t
    (*

    variable

    *)
  3. | Add of aexp * aexp
    (*

    addition

    *)
  4. | Sub of aexp * aexp
    (*

    subtraction

    *)
  5. | Mul of aexp * aexp
    (*

    multiplication

    *)

The aexp type represents integer-valued expressions in the While language. It includes literal constants and has three basic binary operations: addition, subtraction, and multiplication. Each constructor takes one or two sub-expressions of type aexp, allowing arbitrarily nested arithmetic trees (for example, (x + 2) * (y - 1)).

Sourcetype bexp =
  1. | True
  2. | False
  3. | Eq of aexp * aexp
    (*

    equality

    *)
  4. | Le of aexp * aexp
    (*

    less than or equal

    *)
  5. | Gt of aexp * aexp
    (*

    striclty greater than

    *)
  6. | Not of bexp
    (*

    negation

    *)
  7. | And of bexp * bexp
    (*

    conjunction

    *)

The bexp boolean expression captures logical predicates used in conditionals and loops. It provides the Boolean constants (True, False), comparison operators over arithmetic expressions -- equality (Eq), less-than-or-equal (Le), and greater-than (Ge) -- as well as logical negation (Not) and conjunction (And).

With nesting, one can form complex expressions such as (v <= 5 && !(v == 0)).

Sourcetype stmt =
  1. | Skip
  2. | Assign of Var.t * aexp
  3. | Seq of stmt * stmt
  4. | If of bexp * stmt * stmt
  5. | While of bexp * stmt
    (*

    Finally, the stmt type defines the statements of the While language. Skip is a no operation; Assign updates a variable from an arithmetic expression; Seq composes two commands sequentially; If chooses one of two branches based on a boolean test; and While repeatedly executes its body while a condition holds.

    *)
Sourceval pp_aexp : Format.formatter -> aexp -> unit
Sourceval pp_bexp : Format.formatter -> bexp -> unit
Sourceval pp_stmt : Format.formatter -> stmt -> unit