package linksem

  1. Overview
  2. Docs

Module Abstract_linker_scriptSource

Sourcetype binary_relation =
  1. | Eq0
  2. | Lt0
Sourcetype binary_connective =
  1. | And0
    (*

    Conjunction

    *)
  2. | Or0
    (*

    Disjunction

    *)
Sourcetype 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.

Sourcetype 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
Sourcetype 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
Sourcetype memory_image0 =
  1. | MemoryImage of memory_image_formula
Sourceval mk_range : Nat_big_num.num -> Nat_big_num.num -> value_formula