Module Abstract_linker_script

type binary_relation =
| Eq0
| Lt0
type binary_connective =
| And0
| Or0
type expression =
| Var0 of string
| Const of Nat_big_num.num
type value_formula =
| VFTrue
| VFFalse
| VFBinaryRelation of binary_relation * expression
| VFBinaryConnective of binary_connective * value_formula * value_formula
| VFNot of value_formula
type memory_image_formula =
| MIFTrue
| MIFFalse
| MIFExists of string * memory_image_formula
| MIFBinaryRelation of binary_relation * expression * expression
| MIFBinaryConnective of binary_connective * memory_image_formula * memory_image_formula
| MIFAssertValueFormula of expression * value_formula
| MIFNot of memory_image_formula
type memory_image0 =
| MemoryImage of memory_image_formula
val mk_range : Nat_big_num.num -> Nat_big_num.num -> value_formula