extracted/memProperties.mli

   1 open Preamble
   2
   3 open Sets
   4
   5 open Listb
   6
   7 open IO
   8
   9 open IOMonad
  10
  11 open Star
  12
  13 open ClassifyOp
  14
  15 open Events
  16
  17 open Smallstep
  18
  19 open Extra_bool
  20
  21 open Values
  22
  23 open FrontEndVal
  24
  25 open Hide
  26
  27 open ByteValues
  28
  29 open Division
  30
  31 open Z
  32
  33 open BitVectorZ
  34
  35 open Pointers
  36
  37 open GenMem
  38
  39 open FrontEndMem
  40
  41 open Globalenvs
  42
  43 open Csem
  44
  45 open CostLabel
  46
  47 open Coqlib
  48
  49 open Proper
  50
  51 open PositiveMap
  52
  53 open Deqsets
  54
  55 open ErrorMessages
  56
  57 open PreIdentifiers
  58
  59 open Errors
  60
  61 open Extralib
  62
  63 open Lists
  64
  65 open Positive
  66
  67 open Identifiers
  68
  69 open Exp
  70
  71 open Arithmetic
  72
  73 open Vector
  74
  75 open Div_and_mod
  76
  77 open Util
  78
  79 open FoldStuff
  80
  81 open BitVector
  82
  83 open Jmeq
  84
  85 open Russell
  86
  87 open List
  88
  89 open Setoids
  90
  91 open Monad
  92
  93 open Option
  94
  95 open Extranat
  96
  97 open Bool
  98
  99 open Relations
 100
 101 open Nat
 102
 103 open Integers
 104
 105 open Hints_declaration
 106
 107 open Core_notation
 108
 109 open Pts
 110
 111 open Logic
 112
 113 open Types
 114
 115 open AST
 116
 117 open Csyntax
 118
 119 open TypeComparison
 120
 121 open Frontend_misc
 122
 123 open SmallstepExec
 124
 125 open Cexec
 126
 127 val z_of_offset : Pointers.offset -> Z.z
 128
 129 val shiftn : Pointers.offset -> Nat.nat -> Pointers.offset
 130