extracted/frontEndOps.mli

   1 open Preamble
   2
   3 open Proper
   4
   5 open PositiveMap
   6
   7 open Deqsets
   8
   9 open Extralib
  10
  11 open Lists
  12
  13 open Identifiers
  14
  15 open Integers
  16
  17 open AST
  18
  19 open Division
  20
  21 open Exp
  22
  23 open Arithmetic
  24
  25 open Extranat
  26
  27 open Vector
  28
  29 open FoldStuff
  30
  31 open BitVector
  32
  33 open Z
  34
  35 open BitVectorZ
  36
  37 open Pointers
  38
  39 open ErrorMessages
  40
  41 open Option
  42
  43 open Setoids
  44
  45 open Monad
  46
  47 open Positive
  48
  49 open PreIdentifiers
  50
  51 open Errors
  52
  53 open Div_and_mod
  54
  55 open Jmeq
  56
  57 open Russell
  58
  59 open Util
  60
  61 open Bool
  62
  63 open Relations
  64
  65 open Nat
  66
  67 open List
  68
  69 open Hints_declaration
  70
  71 open Core_notation
  72
  73 open Pts
  74
  75 open Logic
  76
  77 open Types
  78
  79 open Coqlib
  80
  81 open Values
  82
  83 open FrontEndVal
  84
  85 open Hide
  86
  87 open ByteValues
  88
  89 open GenMem
  90
  91 open FrontEndMem
  92
  93 type constant =
  94 | Ointconst of AST.intsize * AST.signedness * AST.bvint
  95 | Oaddrsymbol of AST.ident * Nat.nat
  96 | Oaddrstack of Nat.nat
  97
  98 val constant_rect_Type4 :
  99   (AST.intsize -> AST.signedness -> AST.bvint -> 'a1) -> (AST.ident ->
 100   Nat.nat -> 'a1) -> (Nat.nat -> 'a1) -> AST.typ -> constant -> 'a1
 101
 102 val constant_rect_Type5 :
 103   (AST.intsize -> AST.signedness -> AST.bvint -> 'a1) -> (AST.ident ->
 104   Nat.nat -> 'a1) -> (Nat.nat -> 'a1) -> AST.typ -> constant -> 'a1
 105
 106 val constant_rect_Type3 :
 107   (AST.intsize -> AST.signedness -> AST.bvint -> 'a1) -> (AST.ident ->
 108   Nat.nat -> 'a1) -> (Nat.nat -> 'a1) -> AST.typ -> constant -> 'a1
 109
 110 val constant_rect_Type2 :
 111   (AST.intsize -> AST.signedness -> AST.bvint -> 'a1) -> (AST.ident ->
 112   Nat.nat -> 'a1) -> (Nat.nat -> 'a1) -> AST.typ -> constant -> 'a1
 113
 114 val constant_rect_Type1 :
 115   (AST.intsize -> AST.signedness -> AST.bvint -> 'a1) -> (AST.ident ->
 116   Nat.nat -> 'a1) -> (Nat.nat -> 'a1) -> AST.typ -> constant -> 'a1
 117
 118 val constant_rect_Type0 :
 119   (AST.intsize -> AST.signedness -> AST.bvint -> 'a1) -> (AST.ident ->
 120   Nat.nat -> 'a1) -> (Nat.nat -> 'a1) -> AST.typ -> constant -> 'a1
 121
 122 val constant_inv_rect_Type4 :
 123   AST.typ -> constant -> (AST.intsize -> AST.signedness -> AST.bvint -> __ ->
 124   __ -> 'a1) -> (AST.ident -> Nat.nat -> __ -> __ -> 'a1) -> (Nat.nat -> __
 125   -> __ -> 'a1) -> 'a1
 126
 127 val constant_inv_rect_Type3 :
 128   AST.typ -> constant -> (AST.intsize -> AST.signedness -> AST.bvint -> __ ->
 129   __ -> 'a1) -> (AST.ident -> Nat.nat -> __ -> __ -> 'a1) -> (Nat.nat -> __
 130   -> __ -> 'a1) -> 'a1
 131
 132 val constant_inv_rect_Type2 :
 133   AST.typ -> constant -> (AST.intsize -> AST.signedness -> AST.bvint -> __ ->
 134   __ -> 'a1) -> (AST.ident -> Nat.nat -> __ -> __ -> 'a1) -> (Nat.nat -> __
 135   -> __ -> 'a1) -> 'a1
 136
 137 val constant_inv_rect_Type1 :
 138   AST.typ -> constant -> (AST.intsize -> AST.signedness -> AST.bvint -> __ ->
 139   __ -> 'a1) -> (AST.ident -> Nat.nat -> __ -> __ -> 'a1) -> (Nat.nat -> __
 140   -> __ -> 'a1) -> 'a1
 141
 142 val constant_inv_rect_Type0 :
 143   AST.typ -> constant -> (AST.intsize -> AST.signedness -> AST.bvint -> __ ->
 144   __ -> 'a1) -> (AST.ident -> Nat.nat -> __ -> __ -> 'a1) -> (Nat.nat -> __
 145   -> __ -> 'a1) -> 'a1
 146
 147 val constant_discr : AST.typ -> constant -> constant -> __
 148
 149 val constant_jmdiscr : AST.typ -> constant -> constant -> __
 150
 151 type unary_operation =
 152 | Ocastint of AST.intsize * AST.signedness * AST.intsize * AST.signedness
 153 | Onegint of AST.intsize * AST.signedness
 154 | Onotbool of AST.typ * AST.intsize * AST.signedness
 155 | Onotint of AST.intsize * AST.signedness
 156 | Oid of AST.typ
 157 | Optrofint of AST.intsize * AST.signedness
 158 | Ointofptr of AST.intsize * AST.signedness
 159
 160 val unary_operation_rect_Type4 :
 161   (AST.intsize -> AST.signedness -> AST.intsize -> AST.signedness -> 'a1) ->
 162   (AST.intsize -> AST.signedness -> 'a1) -> (AST.typ -> AST.intsize ->
 163   AST.signedness -> __ -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) ->
 164   (AST.typ -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize
 165   -> AST.signedness -> 'a1) -> AST.typ -> AST.typ -> unary_operation -> 'a1
 166
 167 val unary_operation_rect_Type5 :
 168   (AST.intsize -> AST.signedness -> AST.intsize -> AST.signedness -> 'a1) ->
 169   (AST.intsize -> AST.signedness -> 'a1) -> (AST.typ -> AST.intsize ->
 170   AST.signedness -> __ -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) ->
 171   (AST.typ -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize
 172   -> AST.signedness -> 'a1) -> AST.typ -> AST.typ -> unary_operation -> 'a1
 173
 174 val unary_operation_rect_Type3 :
 175   (AST.intsize -> AST.signedness -> AST.intsize -> AST.signedness -> 'a1) ->
 176   (AST.intsize -> AST.signedness -> 'a1) -> (AST.typ -> AST.intsize ->
 177   AST.signedness -> __ -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) ->
 178   (AST.typ -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize
 179   -> AST.signedness -> 'a1) -> AST.typ -> AST.typ -> unary_operation -> 'a1
 180
 181 val unary_operation_rect_Type2 :
 182   (AST.intsize -> AST.signedness -> AST.intsize -> AST.signedness -> 'a1) ->
 183   (AST.intsize -> AST.signedness -> 'a1) -> (AST.typ -> AST.intsize ->
 184   AST.signedness -> __ -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) ->
 185   (AST.typ -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize
 186   -> AST.signedness -> 'a1) -> AST.typ -> AST.typ -> unary_operation -> 'a1
 187
 188 val unary_operation_rect_Type1 :
 189   (AST.intsize -> AST.signedness -> AST.intsize -> AST.signedness -> 'a1) ->
 190   (AST.intsize -> AST.signedness -> 'a1) -> (AST.typ -> AST.intsize ->
 191   AST.signedness -> __ -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) ->
 192   (AST.typ -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize
 193   -> AST.signedness -> 'a1) -> AST.typ -> AST.typ -> unary_operation -> 'a1
 194
 195 val unary_operation_rect_Type0 :
 196   (AST.intsize -> AST.signedness -> AST.intsize -> AST.signedness -> 'a1) ->
 197   (AST.intsize -> AST.signedness -> 'a1) -> (AST.typ -> AST.intsize ->
 198   AST.signedness -> __ -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) ->
 199   (AST.typ -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize
 200   -> AST.signedness -> 'a1) -> AST.typ -> AST.typ -> unary_operation -> 'a1
 201
 202 val unary_operation_inv_rect_Type4 :
 203   AST.typ -> AST.typ -> unary_operation -> (AST.intsize -> AST.signedness ->
 204   AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
 205   AST.signedness -> __ -> __ -> __ -> 'a1) -> (AST.typ -> AST.intsize ->
 206   AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
 207   AST.signedness -> __ -> __ -> __ -> 'a1) -> (AST.typ -> __ -> __ -> __ ->
 208   'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) ->
 209   (AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) -> 'a1
 210
 211 val unary_operation_inv_rect_Type3 :
 212   AST.typ -> AST.typ -> unary_operation -> (AST.intsize -> AST.signedness ->
 213   AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
 214   AST.signedness -> __ -> __ -> __ -> 'a1) -> (AST.typ -> AST.intsize ->
 215   AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
 216   AST.signedness -> __ -> __ -> __ -> 'a1) -> (AST.typ -> __ -> __ -> __ ->
 217   'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) ->
 218   (AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) -> 'a1
 219
 220 val unary_operation_inv_rect_Type2 :
 221   AST.typ -> AST.typ -> unary_operation -> (AST.intsize -> AST.signedness ->
 222   AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
 223   AST.signedness -> __ -> __ -> __ -> 'a1) -> (AST.typ -> AST.intsize ->
 224   AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
 225   AST.signedness -> __ -> __ -> __ -> 'a1) -> (AST.typ -> __ -> __ -> __ ->
 226   'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) ->
 227   (AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) -> 'a1
 228
 229 val unary_operation_inv_rect_Type1 :
 230   AST.typ -> AST.typ -> unary_operation -> (AST.intsize -> AST.signedness ->
 231   AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
 232   AST.signedness -> __ -> __ -> __ -> 'a1) -> (AST.typ -> AST.intsize ->
 233   AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
 234   AST.signedness -> __ -> __ -> __ -> 'a1) -> (AST.typ -> __ -> __ -> __ ->
 235   'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) ->
 236   (AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) -> 'a1
 237
 238 val unary_operation_inv_rect_Type0 :
 239   AST.typ -> AST.typ -> unary_operation -> (AST.intsize -> AST.signedness ->
 240   AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
 241   AST.signedness -> __ -> __ -> __ -> 'a1) -> (AST.typ -> AST.intsize ->
 242   AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
 243   AST.signedness -> __ -> __ -> __ -> 'a1) -> (AST.typ -> __ -> __ -> __ ->
 244   'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) ->
 245   (AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) -> 'a1
 246
 247 val unary_operation_discr :
 248   AST.typ -> AST.typ -> unary_operation -> unary_operation -> __
 249
 250 val unary_operation_jmdiscr :
 251   AST.typ -> AST.typ -> unary_operation -> unary_operation -> __
 252
 253 type binary_operation =
 254 | Oadd of AST.intsize * AST.signedness
 255 | Osub of AST.intsize * AST.signedness
 256 | Omul of AST.intsize * AST.signedness
 257 | Odiv of AST.intsize
 258 | Odivu of AST.intsize
 259 | Omod of AST.intsize
 260 | Omodu of AST.intsize
 261 | Oand of AST.intsize * AST.signedness
 262 | Oor of AST.intsize * AST.signedness
 263 | Oxor of AST.intsize * AST.signedness
 264 | Oshl of AST.intsize * AST.signedness
 265 | Oshr of AST.intsize * AST.signedness
 266 | Oshru of AST.intsize * AST.signedness
 267 | Ocmp of AST.intsize * AST.signedness * AST.signedness * Integers.comparison
 268 | Ocmpu of AST.intsize * AST.signedness * Integers.comparison
 269 | Oaddpi of AST.intsize
 270 | Oaddip of AST.intsize
 271 | Osubpi of AST.intsize
 272 | Osubpp of AST.intsize
 273 | Ocmpp of AST.signedness * Integers.comparison
 274
 275 val binary_operation_rect_Type4 :
 276   (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness ->
 277   'a1) -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> 'a1) ->
 278   (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) ->
 279   (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness ->
 280   'a1) -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize ->
 281   AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) ->
 282   (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness ->
 283   AST.signedness -> Integers.comparison -> 'a1) -> (AST.intsize ->
 284   AST.signedness -> Integers.comparison -> 'a1) -> (AST.intsize -> 'a1) ->
 285   (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) ->
 286   (AST.signedness -> Integers.comparison -> 'a1) -> AST.typ -> AST.typ ->
 287   AST.typ -> binary_operation -> 'a1
 288
 289 val binary_operation_rect_Type5 :
 290   (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness ->
 291   'a1) -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> 'a1) ->
 292   (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) ->
 293   (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness ->
 294   'a1) -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize ->
 295   AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) ->
 296   (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness ->
 297   AST.signedness -> Integers.comparison -> 'a1) -> (AST.intsize ->
 298   AST.signedness -> Integers.comparison -> 'a1) -> (AST.intsize -> 'a1) ->
 299   (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) ->
 300   (AST.signedness -> Integers.comparison -> 'a1) -> AST.typ -> AST.typ ->
 301   AST.typ -> binary_operation -> 'a1
 302
 303 val binary_operation_rect_Type3 :
 304   (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness ->
 305   'a1) -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> 'a1) ->
 306   (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) ->
 307   (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness ->
 308   'a1) -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize ->
 309   AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) ->
 310   (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness ->
 311   AST.signedness -> Integers.comparison -> 'a1) -> (AST.intsize ->
 312   AST.signedness -> Integers.comparison -> 'a1) -> (AST.intsize -> 'a1) ->
 313   (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) ->
 314   (AST.signedness -> Integers.comparison -> 'a1) -> AST.typ -> AST.typ ->
 315   AST.typ -> binary_operation -> 'a1
 316
 317 val binary_operation_rect_Type2 :
 318   (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness ->
 319   'a1) -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> 'a1) ->
 320   (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) ->
 321   (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness ->
 322   'a1) -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize ->
 323   AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) ->
 324   (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness ->
 325   AST.signedness -> Integers.comparison -> 'a1) -> (AST.intsize ->
 326   AST.signedness -> Integers.comparison -> 'a1) -> (AST.intsize -> 'a1) ->
 327   (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) ->
 328   (AST.signedness -> Integers.comparison -> 'a1) -> AST.typ -> AST.typ ->
 329   AST.typ -> binary_operation -> 'a1
 330
 331 val binary_operation_rect_Type1 :
 332   (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness ->
 333   'a1) -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> 'a1) ->
 334   (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) ->
 335   (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness ->
 336   'a1) -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize ->
 337   AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) ->
 338   (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness ->
 339   AST.signedness -> Integers.comparison -> 'a1) -> (AST.intsize ->
 340   AST.signedness -> Integers.comparison -> 'a1) -> (AST.intsize -> 'a1) ->
 341   (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) ->
 342   (AST.signedness -> Integers.comparison -> 'a1) -> AST.typ -> AST.typ ->
 343   AST.typ -> binary_operation -> 'a1
 344
 345 val binary_operation_rect_Type0 :
 346   (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness ->
 347   'a1) -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> 'a1) ->
 348   (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) ->
 349   (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness ->
 350   'a1) -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize ->
 351   AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) ->
 352   (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness ->
 353   AST.signedness -> Integers.comparison -> 'a1) -> (AST.intsize ->
 354   AST.signedness -> Integers.comparison -> 'a1) -> (AST.intsize -> 'a1) ->
 355   (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) ->
 356   (AST.signedness -> Integers.comparison -> 'a1) -> AST.typ -> AST.typ ->
 357   AST.typ -> binary_operation -> 'a1
 358
 359 val binary_operation_inv_rect_Type4 :
 360   AST.typ -> AST.typ -> AST.typ -> binary_operation -> (AST.intsize ->
 361   AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
 362   AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
 363   AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __
 364   -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __ -> __ -> __ -> 'a1) ->
 365   (AST.intsize -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __ ->
 366   __ -> __ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __
 367   -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1)
 368   -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
 369   (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
 370   (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
 371   (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
 372   (AST.intsize -> AST.signedness -> AST.signedness -> Integers.comparison ->
 373   __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> AST.signedness ->
 374   Integers.comparison -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __
 375   -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __ -> __ -> __ -> 'a1)
 376   -> (AST.intsize -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __
 377   -> __ -> __ -> 'a1) -> (AST.signedness -> Integers.comparison -> __ -> __
 378   -> __ -> __ -> 'a1) -> 'a1
 379
 380 val binary_operation_inv_rect_Type3 :
 381   AST.typ -> AST.typ -> AST.typ -> binary_operation -> (AST.intsize ->
 382   AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
 383   AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
 384   AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __
 385   -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __ -> __ -> __ -> 'a1) ->
 386   (AST.intsize -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __ ->
 387   __ -> __ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __
 388   -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1)
 389   -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
 390   (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
 391   (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
 392   (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
 393   (AST.intsize -> AST.signedness -> AST.signedness -> Integers.comparison ->
 394   __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> AST.signedness ->
 395   Integers.comparison -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __
 396   -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __ -> __ -> __ -> 'a1)
 397   -> (AST.intsize -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __
 398   -> __ -> __ -> 'a1) -> (AST.signedness -> Integers.comparison -> __ -> __
 399   -> __ -> __ -> 'a1) -> 'a1
 400
 401 val binary_operation_inv_rect_Type2 :
 402   AST.typ -> AST.typ -> AST.typ -> binary_operation -> (AST.intsize ->
 403   AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
 404   AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
 405   AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __
 406   -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __ -> __ -> __ -> 'a1) ->
 407   (AST.intsize -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __ ->
 408   __ -> __ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __
 409   -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1)
 410   -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
 411   (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
 412   (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
 413   (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
 414   (AST.intsize -> AST.signedness -> AST.signedness -> Integers.comparison ->
 415   __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> AST.signedness ->
 416   Integers.comparison -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __
 417   -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __ -> __ -> __ -> 'a1)
 418   -> (AST.intsize -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __
 419   -> __ -> __ -> 'a1) -> (AST.signedness -> Integers.comparison -> __ -> __
 420   -> __ -> __ -> 'a1) -> 'a1
 421
 422 val binary_operation_inv_rect_Type1 :
 423   AST.typ -> AST.typ -> AST.typ -> binary_operation -> (AST.intsize ->
 424   AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
 425   AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
 426   AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __
 427   -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __ -> __ -> __ -> 'a1) ->
 428   (AST.intsize -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __ ->
 429   __ -> __ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __
 430   -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1)
 431   -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
 432   (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
 433   (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
 434   (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
 435   (AST.intsize -> AST.signedness -> AST.signedness -> Integers.comparison ->
 436   __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> AST.signedness ->
 437   Integers.comparison -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __
 438   -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __ -> __ -> __ -> 'a1)
 439   -> (AST.intsize -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __
 440   -> __ -> __ -> 'a1) -> (AST.signedness -> Integers.comparison -> __ -> __
 441   -> __ -> __ -> 'a1) -> 'a1
 442
 443 val binary_operation_inv_rect_Type0 :
 444   AST.typ -> AST.typ -> AST.typ -> binary_operation -> (AST.intsize ->
 445   AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
 446   AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
 447   AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __
 448   -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __ -> __ -> __ -> 'a1) ->
 449   (AST.intsize -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __ ->
 450   __ -> __ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __
 451   -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1)
 452   -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
 453   (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
 454   (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
 455   (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
 456   (AST.intsize -> AST.signedness -> AST.signedness -> Integers.comparison ->
 457   __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> AST.signedness ->
 458   Integers.comparison -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __
 459   -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __ -> __ -> __ -> 'a1)
 460   -> (AST.intsize -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __
 461   -> __ -> __ -> 'a1) -> (AST.signedness -> Integers.comparison -> __ -> __
 462   -> __ -> __ -> 'a1) -> 'a1
 463
 464 val binary_operation_discr :
 465   AST.typ -> AST.typ -> AST.typ -> binary_operation -> binary_operation -> __
 466
 467 val binary_operation_jmdiscr :
 468   AST.typ -> AST.typ -> AST.typ -> binary_operation -> binary_operation -> __
 469
 470 val eval_constant :
 471   AST.typ -> (AST.ident -> Pointers.block Types.option) -> Pointers.block ->
 472   constant -> Values.val0 Types.option
 473
 474 val eval_unop :
 475   AST.typ -> AST.typ -> unary_operation -> Values.val0 -> Values.val0
 476   Types.option
 477
 478 val eval_compare_mismatch : Integers.comparison -> Values.val0 Types.option
 479
 480 val ev_add : Values.val0 -> Values.val0 -> Values.val0 Types.option
 481
 482 val ev_sub : Values.val0 -> Values.val0 -> Values.val0 Types.option
 483
 484 val ev_addpi : Values.val0 -> Values.val0 -> Values.val0 Types.option
 485
 486 val ev_subpi : Values.val0 -> Values.val0 -> Values.val0 Types.option
 487
 488 val ev_subpp :
 489   AST.intsize -> Values.val0 -> Values.val0 -> Values.val0 Types.option
 490
 491 val ev_mul : Values.val0 -> Values.val0 -> Values.val0 Types.option
 492
 493 val ev_divs : Values.val0 -> Values.val0 -> Values.val0 Types.option
 494
 495 val ev_mods : Values.val0 -> Values.val0 -> Values.val0 Types.option
 496
 497 val ev_divu : Values.val0 -> Values.val0 -> Values.val0 Types.option
 498
 499 val ev_modu : Values.val0 -> Values.val0 -> Values.val0 Types.option
 500
 501 val ev_and : Values.val0 -> Values.val0 -> Values.val0 Types.option
 502
 503 val ev_or : Values.val0 -> Values.val0 -> Values.val0 Types.option
 504
 505 val ev_xor : Values.val0 -> Values.val0 -> Values.val0 Types.option
 506
 507 val ev_shl : Values.val0 -> Values.val0 -> Values.val0 Types.option
 508
 509 val ev_shr : Values.val0 -> Values.val0 -> Values.val0 Types.option
 510
 511 val ev_shru : Values.val0 -> Values.val0 -> Values.val0 Types.option
 512
 513 val fEtrue : Values.val0
 514
 515 val fEfalse : Values.val0
 516
 517 val fE_of_bool : Bool.bool -> Values.val0
 518
 519 val ev_cmp_match : Integers.comparison -> Values.val0 Types.option
 520
 521 val ev_cmp_mismatch : Integers.comparison -> Values.val0 Types.option
 522
 523 val ev_cmp :
 524   Integers.comparison -> Values.val0 -> Values.val0 -> Values.val0
 525   Types.option
 526
 527 val ev_cmpp :
 528   GenMem.mem -> Integers.comparison -> Values.val0 -> Values.val0 ->
 529   Values.val0 Types.option
 530
 531 val ev_cmpu :
 532   Integers.comparison -> Values.val0 -> Values.val0 -> Values.val0
 533   Types.option
 534
 535 val eval_binop :
 536   GenMem.mem -> AST.typ -> AST.typ -> AST.typ -> binary_operation ->
 537   Values.val0 -> Values.val0 -> Values.val0 Types.option
 538