extracted/i8051.mli

   1 open Preamble
   2
   3 open Bool
   4
   5 open Hints_declaration
   6
   7 open Core_notation
   8
   9 open Pts
  10
  11 open Logic
  12
  13 open Relations
  14
  15 open Nat
  16
  17 open Jmeq
  18
  19 open Exp
  20
  21 open Setoids
  22
  23 open Monad
  24
  25 open Option
  26
  27 open Extranat
  28
  29 open Vector
  30
  31 open Div_and_mod
  32
  33 open Russell
  34
  35 open Types
  36
  37 open List
  38
  39 open Util
  40
  41 open FoldStuff
  42
  43 open BitVector
  44
  45 open Arithmetic
  46
  47 val int_size : BitVector.bitVector
  48
  49 val ptr_size : BitVector.bitVector
  50
  51 val alignment : 'a1 Types.option
  52
  53 type register =
  54 | Register00
  55 | Register01
  56 | Register02
  57 | Register03
  58 | Register04
  59 | Register05
  60 | Register06
  61 | Register07
  62 | Register10
  63 | Register11
  64 | Register12
  65 | Register13
  66 | Register14
  67 | Register15
  68 | Register16
  69 | Register17
  70 | Register20
  71 | Register21
  72 | Register22
  73 | Register23
  74 | Register24
  75 | Register25
  76 | Register26
  77 | Register27
  78 | Register30
  79 | Register31
  80 | Register32
  81 | Register33
  82 | Register34
  83 | Register35
  84 | Register36
  85 | Register37
  86 | RegisterA
  87 | RegisterB
  88 | RegisterDPL
  89 | RegisterDPH
  90 | RegisterCarry
  91
  92 val register_rect_Type4 :
  93   'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
  94   -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 ->
  95   'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
  96   -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> register -> 'a1
  97
  98 val register_rect_Type5 :
  99   'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
 100   -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 ->
 101   'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
 102   -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> register -> 'a1
 103
 104 val register_rect_Type3 :
 105   'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
 106   -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 ->
 107   'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
 108   -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> register -> 'a1
 109
 110 val register_rect_Type2 :
 111   'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
 112   -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 ->
 113   'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
 114   -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> register -> 'a1
 115
 116 val register_rect_Type1 :
 117   'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
 118   -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 ->
 119   'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
 120   -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> register -> 'a1
 121
 122 val register_rect_Type0 :
 123   'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
 124   -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 ->
 125   'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
 126   -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> register -> 'a1
 127
 128 val register_inv_rect_Type4 :
 129   register -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
 130   -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
 131   -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
 132   -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
 133   -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
 134   -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
 135   -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
 136   -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
 137
 138 val register_inv_rect_Type3 :
 139   register -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
 140   -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
 141   -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
 142   -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
 143   -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
 144   -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
 145   -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
 146   -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
 147
 148 val register_inv_rect_Type2 :
 149   register -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
 150   -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
 151   -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
 152   -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
 153   -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
 154   -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
 155   -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
 156   -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
 157
 158 val register_inv_rect_Type1 :
 159   register -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
 160   -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
 161   -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
 162   -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
 163   -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
 164   -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
 165   -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
 166   -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
 167
 168 val register_inv_rect_Type0 :
 169   register -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
 170   -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
 171   -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
 172   -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
 173   -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
 174   -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
 175   -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
 176   -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
 177
 178 val register_discr : register -> register -> __
 179
 180 val register_jmdiscr : register -> register -> __
 181
 182 val nat_of_register : register -> Nat.nat
 183
 184 val physical_register_count : Nat.nat
 185
 186 val bitvector_of_register : register -> BitVector.bitVector
 187
 188 val eq_Register : register -> register -> Bool.bool
 189
 190 val registerSST : register
 191
 192 val registerST0 : register
 193
 194 val registerST1 : register
 195
 196 val registerST2 : register
 197
 198 val registerST3 : register
 199
 200 val registerSTS : register List.list
 201
 202 val registerSPL : register
 203
 204 val registerSPH : register
 205
 206 val registerParams : register List.list
 207
 208 val registers : register List.list
 209
 210 val registerRets : register List.list
 211
 212 val registerCallerSaved : register List.list
 213
 214 val registerCalleeSaved : register List.list
 215
 216 val registersForbidden : register List.list
 217
 218 val registersAllocatable : register List.list
 219