extracted/bEMem.mli

   1 open Preamble
   2
   3 open Hide
   4
   5 open Proper
   6
   7 open PositiveMap
   8
   9 open Deqsets
  10
  11 open ErrorMessages
  12
  13 open PreIdentifiers
  14
  15 open Errors
  16
  17 open Extralib
  18
  19 open Lists
  20
  21 open Identifiers
  22
  23 open Integers
  24
  25 open AST
  26
  27 open Division
  28
  29 open Exp
  30
  31 open Arithmetic
  32
  33 open Setoids
  34
  35 open Monad
  36
  37 open Option
  38
  39 open Extranat
  40
  41 open Vector
  42
  43 open Div_and_mod
  44
  45 open Jmeq
  46
  47 open Russell
  48
  49 open List
  50
  51 open Util
  52
  53 open FoldStuff
  54
  55 open BitVector
  56
  57 open Types
  58
  59 open Bool
  60
  61 open Relations
  62
  63 open Nat
  64
  65 open Hints_declaration
  66
  67 open Core_notation
  68
  69 open Pts
  70
  71 open Logic
  72
  73 open Positive
  74
  75 open Z
  76
  77 open BitVectorZ
  78
  79 open Pointers
  80
  81 open ByteValues
  82
  83 open GenMem
  84
  85 type bemem = GenMem.mem
  86
  87 val is_addressable : AST.region -> Bool.bool
  88
  89 type address = (ByteValues.beval, ByteValues.beval) Types.prod
  90
  91 val pointer_of_address : address -> Pointers.pointer Errors.res
  92