package linksem

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type
type binary_relation =
  1. | Eq0
  2. | Lt0
type binary_connective =
  1. | And0
    (*

    Conjunction

    *)
  2. | Or0
    (*

    Disjunction

    *)
type expression =
  1. | Var0 of string
    (*

    Ranges over memory addresses

    *)
  2. | Const of Nat_big_num.num
    (*

    Fixed memory address

    *)

The type expression denotes addresses, whether known or to be ascertained.

type value_formula =
  1. | VFTrue
  2. | VFFalse
  3. | VFBinaryRelation of binary_relation * expression
  4. | VFBinaryConnective of binary_connective * value_formula * value_formula
  5. | VFNot of value_formula
type memory_image_formula =
  1. | MIFTrue
  2. | MIFFalse
  3. | MIFExists of string * memory_image_formula
  4. | MIFBinaryRelation of binary_relation * expression * expression
  5. | MIFBinaryConnective of binary_connective * memory_image_formula * memory_image_formula
  6. | MIFAssertValueFormula of expression * value_formula
  7. | MIFNot of memory_image_formula
type memory_image0 =
  1. | MemoryImage of memory_image_formula
OCaml

Innovation. Community. Security.