extracted/frontEndOps.ml

   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 let rec constant_rect_Type4 h_Ointconst h_Oaddrsymbol h_Oaddrstack x_13118 = function
 102 | Ointconst (sz, sg, x_13120) -> h_Ointconst sz sg x_13120
 103 | Oaddrsymbol (x_13122, x_13121) -> h_Oaddrsymbol x_13122 x_13121
 104 | Oaddrstack x_13123 -> h_Oaddrstack x_13123
 105
 106 (** val constant_rect_Type5 :
 107     (AST.intsize -> AST.signedness -> AST.bvint -> 'a1) -> (AST.ident ->
 108     Nat.nat -> 'a1) -> (Nat.nat -> 'a1) -> AST.typ -> constant -> 'a1 **)
 109 let rec constant_rect_Type5 h_Ointconst h_Oaddrsymbol h_Oaddrstack x_13127 = function
 110 | Ointconst (sz, sg, x_13129) -> h_Ointconst sz sg x_13129
 111 | Oaddrsymbol (x_13131, x_13130) -> h_Oaddrsymbol x_13131 x_13130
 112 | Oaddrstack x_13132 -> h_Oaddrstack x_13132
 113
 114 (** val constant_rect_Type3 :
 115     (AST.intsize -> AST.signedness -> AST.bvint -> 'a1) -> (AST.ident ->
 116     Nat.nat -> 'a1) -> (Nat.nat -> 'a1) -> AST.typ -> constant -> 'a1 **)
 117 let rec constant_rect_Type3 h_Ointconst h_Oaddrsymbol h_Oaddrstack x_13136 = function
 118 | Ointconst (sz, sg, x_13138) -> h_Ointconst sz sg x_13138
 119 | Oaddrsymbol (x_13140, x_13139) -> h_Oaddrsymbol x_13140 x_13139
 120 | Oaddrstack x_13141 -> h_Oaddrstack x_13141
 121
 122 (** val constant_rect_Type2 :
 123     (AST.intsize -> AST.signedness -> AST.bvint -> 'a1) -> (AST.ident ->
 124     Nat.nat -> 'a1) -> (Nat.nat -> 'a1) -> AST.typ -> constant -> 'a1 **)
 125 let rec constant_rect_Type2 h_Ointconst h_Oaddrsymbol h_Oaddrstack x_13145 = function
 126 | Ointconst (sz, sg, x_13147) -> h_Ointconst sz sg x_13147
 127 | Oaddrsymbol (x_13149, x_13148) -> h_Oaddrsymbol x_13149 x_13148
 128 | Oaddrstack x_13150 -> h_Oaddrstack x_13150
 129
 130 (** val constant_rect_Type1 :
 131     (AST.intsize -> AST.signedness -> AST.bvint -> 'a1) -> (AST.ident ->
 132     Nat.nat -> 'a1) -> (Nat.nat -> 'a1) -> AST.typ -> constant -> 'a1 **)
 133 let rec constant_rect_Type1 h_Ointconst h_Oaddrsymbol h_Oaddrstack x_13154 = function
 134 | Ointconst (sz, sg, x_13156) -> h_Ointconst sz sg x_13156
 135 | Oaddrsymbol (x_13158, x_13157) -> h_Oaddrsymbol x_13158 x_13157
 136 | Oaddrstack x_13159 -> h_Oaddrstack x_13159
 137
 138 (** val constant_rect_Type0 :
 139     (AST.intsize -> AST.signedness -> AST.bvint -> 'a1) -> (AST.ident ->
 140     Nat.nat -> 'a1) -> (Nat.nat -> 'a1) -> AST.typ -> constant -> 'a1 **)
 141 let rec constant_rect_Type0 h_Ointconst h_Oaddrsymbol h_Oaddrstack x_13163 = function
 142 | Ointconst (sz, sg, x_13165) -> h_Ointconst sz sg x_13165
 143 | Oaddrsymbol (x_13167, x_13166) -> h_Oaddrsymbol x_13167 x_13166
 144 | Oaddrstack x_13168 -> h_Oaddrstack x_13168
 145
 146 (** val constant_inv_rect_Type4 :
 147     AST.typ -> constant -> (AST.intsize -> AST.signedness -> AST.bvint -> __
 148     -> __ -> 'a1) -> (AST.ident -> Nat.nat -> __ -> __ -> 'a1) -> (Nat.nat ->
 149     __ -> __ -> 'a1) -> 'a1 **)
 150 let constant_inv_rect_Type4 x1 hterm h1 h2 h3 =
 151   let hcut = constant_rect_Type4 h1 h2 h3 x1 hterm in hcut __ __
 152
 153 (** val constant_inv_rect_Type3 :
 154     AST.typ -> constant -> (AST.intsize -> AST.signedness -> AST.bvint -> __
 155     -> __ -> 'a1) -> (AST.ident -> Nat.nat -> __ -> __ -> 'a1) -> (Nat.nat ->
 156     __ -> __ -> 'a1) -> 'a1 **)
 157 let constant_inv_rect_Type3 x1 hterm h1 h2 h3 =
 158   let hcut = constant_rect_Type3 h1 h2 h3 x1 hterm in hcut __ __
 159
 160 (** val constant_inv_rect_Type2 :
 161     AST.typ -> constant -> (AST.intsize -> AST.signedness -> AST.bvint -> __
 162     -> __ -> 'a1) -> (AST.ident -> Nat.nat -> __ -> __ -> 'a1) -> (Nat.nat ->
 163     __ -> __ -> 'a1) -> 'a1 **)
 164 let constant_inv_rect_Type2 x1 hterm h1 h2 h3 =
 165   let hcut = constant_rect_Type2 h1 h2 h3 x1 hterm in hcut __ __
 166
 167 (** val constant_inv_rect_Type1 :
 168     AST.typ -> constant -> (AST.intsize -> AST.signedness -> AST.bvint -> __
 169     -> __ -> 'a1) -> (AST.ident -> Nat.nat -> __ -> __ -> 'a1) -> (Nat.nat ->
 170     __ -> __ -> 'a1) -> 'a1 **)
 171 let constant_inv_rect_Type1 x1 hterm h1 h2 h3 =
 172   let hcut = constant_rect_Type1 h1 h2 h3 x1 hterm in hcut __ __
 173
 174 (** val constant_inv_rect_Type0 :
 175     AST.typ -> constant -> (AST.intsize -> AST.signedness -> AST.bvint -> __
 176     -> __ -> 'a1) -> (AST.ident -> Nat.nat -> __ -> __ -> 'a1) -> (Nat.nat ->
 177     __ -> __ -> 'a1) -> 'a1 **)
 178 let constant_inv_rect_Type0 x1 hterm h1 h2 h3 =
 179   let hcut = constant_rect_Type0 h1 h2 h3 x1 hterm in hcut __ __
 180
 181 (** val constant_discr : AST.typ -> constant -> constant -> __ **)
 182 let constant_discr a1 x y =
 183   Logic.eq_rect_Type2 x
 184     (match x with
 185      | Ointconst (a0, a10, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
 186      | Oaddrsymbol (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
 187      | Oaddrstack a0 -> Obj.magic (fun _ dH -> dH __)) y
 188
 189 (** val constant_jmdiscr : AST.typ -> constant -> constant -> __ **)
 190 let constant_jmdiscr a1 x y =
 191   Logic.eq_rect_Type2 x
 192     (match x with
 193      | Ointconst (a0, a10, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
 194      | Oaddrsymbol (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
 195      | Oaddrstack a0 -> Obj.magic (fun _ dH -> dH __)) y
 196
 197 type unary_operation =
 198 | Ocastint of AST.intsize * AST.signedness * AST.intsize * AST.signedness
 199 | Onegint of AST.intsize * AST.signedness
 200 | Onotbool of AST.typ * AST.intsize * AST.signedness
 201 | Onotint of AST.intsize * AST.signedness
 202 | Oid of AST.typ
 203 | Optrofint of AST.intsize * AST.signedness
 204 | Ointofptr of AST.intsize * AST.signedness
 205
 206 (** val unary_operation_rect_Type4 :
 207     (AST.intsize -> AST.signedness -> AST.intsize -> AST.signedness -> 'a1)
 208     -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.typ -> AST.intsize ->
 209     AST.signedness -> __ -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) ->
 210     (AST.typ -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) ->
 211     (AST.intsize -> AST.signedness -> 'a1) -> AST.typ -> AST.typ ->
 212     unary_operation -> 'a1 **)
 213 let rec unary_operation_rect_Type4 h_Ocastint h_Onegint h_Onotbool h_Onotint h_Oid h_Optrofint h_Ointofptr x_13238 x_13237 = function
 214 | Ocastint (sz, sg, sz', sg') -> h_Ocastint sz sg sz' sg'
 215 | Onegint (sz, sg) -> h_Onegint sz sg
 216 | Onotbool (t, sz, sg) -> h_Onotbool t sz sg __
 217 | Onotint (sz, sg) -> h_Onotint sz sg
 218 | Oid t -> h_Oid t
 219 | Optrofint (sz, sg) -> h_Optrofint sz sg
 220 | Ointofptr (sz, sg) -> h_Ointofptr sz sg
 221
 222 (** val unary_operation_rect_Type5 :
 223     (AST.intsize -> AST.signedness -> AST.intsize -> AST.signedness -> 'a1)
 224     -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.typ -> AST.intsize ->
 225     AST.signedness -> __ -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) ->
 226     (AST.typ -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) ->
 227     (AST.intsize -> AST.signedness -> 'a1) -> AST.typ -> AST.typ ->
 228     unary_operation -> 'a1 **)
 229 let rec unary_operation_rect_Type5 h_Ocastint h_Onegint h_Onotbool h_Onotint h_Oid h_Optrofint h_Ointofptr x_13249 x_13248 = function
 230 | Ocastint (sz, sg, sz', sg') -> h_Ocastint sz sg sz' sg'
 231 | Onegint (sz, sg) -> h_Onegint sz sg
 232 | Onotbool (t, sz, sg) -> h_Onotbool t sz sg __
 233 | Onotint (sz, sg) -> h_Onotint sz sg
 234 | Oid t -> h_Oid t
 235 | Optrofint (sz, sg) -> h_Optrofint sz sg
 236 | Ointofptr (sz, sg) -> h_Ointofptr sz sg
 237
 238 (** val unary_operation_rect_Type3 :
 239     (AST.intsize -> AST.signedness -> AST.intsize -> AST.signedness -> 'a1)
 240     -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.typ -> AST.intsize ->
 241     AST.signedness -> __ -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) ->
 242     (AST.typ -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) ->
 243     (AST.intsize -> AST.signedness -> 'a1) -> AST.typ -> AST.typ ->
 244     unary_operation -> 'a1 **)
 245 let rec unary_operation_rect_Type3 h_Ocastint h_Onegint h_Onotbool h_Onotint h_Oid h_Optrofint h_Ointofptr x_13260 x_13259 = function
 246 | Ocastint (sz, sg, sz', sg') -> h_Ocastint sz sg sz' sg'
 247 | Onegint (sz, sg) -> h_Onegint sz sg
 248 | Onotbool (t, sz, sg) -> h_Onotbool t sz sg __
 249 | Onotint (sz, sg) -> h_Onotint sz sg
 250 | Oid t -> h_Oid t
 251 | Optrofint (sz, sg) -> h_Optrofint sz sg
 252 | Ointofptr (sz, sg) -> h_Ointofptr sz sg
 253
 254 (** val unary_operation_rect_Type2 :
 255     (AST.intsize -> AST.signedness -> AST.intsize -> AST.signedness -> 'a1)
 256     -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.typ -> AST.intsize ->
 257     AST.signedness -> __ -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) ->
 258     (AST.typ -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) ->
 259     (AST.intsize -> AST.signedness -> 'a1) -> AST.typ -> AST.typ ->
 260     unary_operation -> 'a1 **)
 261 let rec unary_operation_rect_Type2 h_Ocastint h_Onegint h_Onotbool h_Onotint h_Oid h_Optrofint h_Ointofptr x_13271 x_13270 = function
 262 | Ocastint (sz, sg, sz', sg') -> h_Ocastint sz sg sz' sg'
 263 | Onegint (sz, sg) -> h_Onegint sz sg
 264 | Onotbool (t, sz, sg) -> h_Onotbool t sz sg __
 265 | Onotint (sz, sg) -> h_Onotint sz sg
 266 | Oid t -> h_Oid t
 267 | Optrofint (sz, sg) -> h_Optrofint sz sg
 268 | Ointofptr (sz, sg) -> h_Ointofptr sz sg
 269
 270 (** val unary_operation_rect_Type1 :
 271     (AST.intsize -> AST.signedness -> AST.intsize -> AST.signedness -> 'a1)
 272     -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.typ -> AST.intsize ->
 273     AST.signedness -> __ -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) ->
 274     (AST.typ -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) ->
 275     (AST.intsize -> AST.signedness -> 'a1) -> AST.typ -> AST.typ ->
 276     unary_operation -> 'a1 **)
 277 let rec unary_operation_rect_Type1 h_Ocastint h_Onegint h_Onotbool h_Onotint h_Oid h_Optrofint h_Ointofptr x_13282 x_13281 = function
 278 | Ocastint (sz, sg, sz', sg') -> h_Ocastint sz sg sz' sg'
 279 | Onegint (sz, sg) -> h_Onegint sz sg
 280 | Onotbool (t, sz, sg) -> h_Onotbool t sz sg __
 281 | Onotint (sz, sg) -> h_Onotint sz sg
 282 | Oid t -> h_Oid t
 283 | Optrofint (sz, sg) -> h_Optrofint sz sg
 284 | Ointofptr (sz, sg) -> h_Ointofptr sz sg
 285
 286 (** val unary_operation_rect_Type0 :
 287     (AST.intsize -> AST.signedness -> AST.intsize -> AST.signedness -> 'a1)
 288     -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.typ -> AST.intsize ->
 289     AST.signedness -> __ -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) ->
 290     (AST.typ -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) ->
 291     (AST.intsize -> AST.signedness -> 'a1) -> AST.typ -> AST.typ ->
 292     unary_operation -> 'a1 **)
 293 let rec unary_operation_rect_Type0 h_Ocastint h_Onegint h_Onotbool h_Onotint h_Oid h_Optrofint h_Ointofptr x_13293 x_13292 = function
 294 | Ocastint (sz, sg, sz', sg') -> h_Ocastint sz sg sz' sg'
 295 | Onegint (sz, sg) -> h_Onegint sz sg
 296 | Onotbool (t, sz, sg) -> h_Onotbool t sz sg __
 297 | Onotint (sz, sg) -> h_Onotint sz sg
 298 | Oid t -> h_Oid t
 299 | Optrofint (sz, sg) -> h_Optrofint sz sg
 300 | Ointofptr (sz, sg) -> h_Ointofptr sz sg
 301
 302 (** val unary_operation_inv_rect_Type4 :
 303     AST.typ -> AST.typ -> unary_operation -> (AST.intsize -> AST.signedness
 304     -> AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) ->
 305     (AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) -> (AST.typ ->
 306     AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
 307     (AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) -> (AST.typ ->
 308     __ -> __ -> __ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ ->
 309     __ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) ->
 310     'a1 **)
 311 let unary_operation_inv_rect_Type4 x1 x2 hterm h1 h2 h3 h4 h5 h6 h7 =
 312   let hcut = unary_operation_rect_Type4 h1 h2 h3 h4 h5 h6 h7 x1 x2 hterm in
 313   hcut __ __ __
 314
 315 (** val unary_operation_inv_rect_Type3 :
 316     AST.typ -> AST.typ -> unary_operation -> (AST.intsize -> AST.signedness
 317     -> AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) ->
 318     (AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) -> (AST.typ ->
 319     AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
 320     (AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) -> (AST.typ ->
 321     __ -> __ -> __ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ ->
 322     __ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) ->
 323     'a1 **)
 324 let unary_operation_inv_rect_Type3 x1 x2 hterm h1 h2 h3 h4 h5 h6 h7 =
 325   let hcut = unary_operation_rect_Type3 h1 h2 h3 h4 h5 h6 h7 x1 x2 hterm in
 326   hcut __ __ __
 327
 328 (** val unary_operation_inv_rect_Type2 :
 329     AST.typ -> AST.typ -> unary_operation -> (AST.intsize -> AST.signedness
 330     -> AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) ->
 331     (AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) -> (AST.typ ->
 332     AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
 333     (AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) -> (AST.typ ->
 334     __ -> __ -> __ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ ->
 335     __ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) ->
 336     'a1 **)
 337 let unary_operation_inv_rect_Type2 x1 x2 hterm h1 h2 h3 h4 h5 h6 h7 =
 338   let hcut = unary_operation_rect_Type2 h1 h2 h3 h4 h5 h6 h7 x1 x2 hterm in
 339   hcut __ __ __
 340
 341 (** val unary_operation_inv_rect_Type1 :
 342     AST.typ -> AST.typ -> unary_operation -> (AST.intsize -> AST.signedness
 343     -> AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) ->
 344     (AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) -> (AST.typ ->
 345     AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
 346     (AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) -> (AST.typ ->
 347     __ -> __ -> __ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ ->
 348     __ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) ->
 349     'a1 **)
 350 let unary_operation_inv_rect_Type1 x1 x2 hterm h1 h2 h3 h4 h5 h6 h7 =
 351   let hcut = unary_operation_rect_Type1 h1 h2 h3 h4 h5 h6 h7 x1 x2 hterm in
 352   hcut __ __ __
 353
 354 (** val unary_operation_inv_rect_Type0 :
 355     AST.typ -> AST.typ -> unary_operation -> (AST.intsize -> AST.signedness
 356     -> AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) ->
 357     (AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) -> (AST.typ ->
 358     AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
 359     (AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) -> (AST.typ ->
 360     __ -> __ -> __ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ ->
 361     __ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) ->
 362     'a1 **)
 363 let unary_operation_inv_rect_Type0 x1 x2 hterm h1 h2 h3 h4 h5 h6 h7 =
 364   let hcut = unary_operation_rect_Type0 h1 h2 h3 h4 h5 h6 h7 x1 x2 hterm in
 365   hcut __ __ __
 366
 367 (** val unary_operation_discr :
 368     AST.typ -> AST.typ -> unary_operation -> unary_operation -> __ **)
 369 let unary_operation_discr a1 a2 x y =
 370   Logic.eq_rect_Type2 x
 371     (match x with
 372      | Ocastint (a0, a10, a20, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
 373      | Onegint (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
 374      | Onotbool (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __ __)
 375      | Onotint (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
 376      | Oid a0 -> Obj.magic (fun _ dH -> dH __)
 377      | Optrofint (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
 378      | Ointofptr (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)) y
 379
 380 (** val unary_operation_jmdiscr :
 381     AST.typ -> AST.typ -> unary_operation -> unary_operation -> __ **)
 382 let unary_operation_jmdiscr a1 a2 x y =
 383   Logic.eq_rect_Type2 x
 384     (match x with
 385      | Ocastint (a0, a10, a20, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
 386      | Onegint (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
 387      | Onotbool (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __ __)
 388      | Onotint (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
 389      | Oid a0 -> Obj.magic (fun _ dH -> dH __)
 390      | Optrofint (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
 391      | Ointofptr (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)) y
 392
 393 type binary_operation =
 394 | Oadd of AST.intsize * AST.signedness
 395 | Osub of AST.intsize * AST.signedness
 396 | Omul of AST.intsize * AST.signedness
 397 | Odiv of AST.intsize
 398 | Odivu of AST.intsize
 399 | Omod of AST.intsize
 400 | Omodu of AST.intsize
 401 | Oand of AST.intsize * AST.signedness
 402 | Oor of AST.intsize * AST.signedness
 403 | Oxor of AST.intsize * AST.signedness
 404 | Oshl of AST.intsize * AST.signedness
 405 | Oshr of AST.intsize * AST.signedness
 406 | Oshru of AST.intsize * AST.signedness
 407 | Ocmp of AST.intsize * AST.signedness * AST.signedness * Integers.comparison
 408 | Ocmpu of AST.intsize * AST.signedness * Integers.comparison
 409 | Oaddpi of AST.intsize
 410 | Oaddip of AST.intsize
 411 | Osubpi of AST.intsize
 412 | Osubpp of AST.intsize
 413 | Ocmpp of AST.signedness * Integers.comparison
 414
 415 (** val binary_operation_rect_Type4 :
 416     (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness
 417     -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> 'a1)
 418     -> (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) -> (AST.intsize -> 'a1)
 419     -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize ->
 420     AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) ->
 421     (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness
 422     -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize ->
 423     AST.signedness -> AST.signedness -> Integers.comparison -> 'a1) ->
 424     (AST.intsize -> AST.signedness -> Integers.comparison -> 'a1) ->
 425     (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) ->
 426     (AST.intsize -> 'a1) -> (AST.signedness -> Integers.comparison -> 'a1) ->
 427     AST.typ -> AST.typ -> AST.typ -> binary_operation -> 'a1 **)
 428 let rec binary_operation_rect_Type4 h_Oadd h_Osub h_Omul h_Odiv h_Odivu h_Omod h_Omodu h_Oand h_Oor h_Oxor h_Oshl h_Oshr h_Oshru h_Ocmp h_Ocmpu h_Oaddpi h_Oaddip h_Osubpi h_Osubpp h_Ocmpp x_13398 x_13397 x_13396 = function
 429 | Oadd (sz, sg) -> h_Oadd sz sg
 430 | Osub (sz, sg) -> h_Osub sz sg
 431 | Omul (sz, sg) -> h_Omul sz sg
 432 | Odiv sz -> h_Odiv sz
 433 | Odivu sz -> h_Odivu sz
 434 | Omod sz -> h_Omod sz
 435 | Omodu sz -> h_Omodu sz
 436 | Oand (sz, sg) -> h_Oand sz sg
 437 | Oor (sz, sg) -> h_Oor sz sg
 438 | Oxor (sz, sg) -> h_Oxor sz sg
 439 | Oshl (sz, sg) -> h_Oshl sz sg
 440 | Oshr (sz, sg) -> h_Oshr sz sg
 441 | Oshru (sz, sg) -> h_Oshru sz sg
 442 | Ocmp (sz, sg, sg', x_13400) -> h_Ocmp sz sg sg' x_13400
 443 | Ocmpu (sz, sg', x_13401) -> h_Ocmpu sz sg' x_13401
 444 | Oaddpi sz -> h_Oaddpi sz
 445 | Oaddip sz -> h_Oaddip sz
 446 | Osubpi sz -> h_Osubpi sz
 447 | Osubpp sz -> h_Osubpp sz
 448 | Ocmpp (sg', x_13402) -> h_Ocmpp sg' x_13402
 449
 450 (** val binary_operation_rect_Type5 :
 451     (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness
 452     -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> 'a1)
 453     -> (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) -> (AST.intsize -> 'a1)
 454     -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize ->
 455     AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) ->
 456     (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness
 457     -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize ->
 458     AST.signedness -> AST.signedness -> Integers.comparison -> 'a1) ->
 459     (AST.intsize -> AST.signedness -> Integers.comparison -> 'a1) ->
 460     (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) ->
 461     (AST.intsize -> 'a1) -> (AST.signedness -> Integers.comparison -> 'a1) ->
 462     AST.typ -> AST.typ -> AST.typ -> binary_operation -> 'a1 **)
 463 let rec binary_operation_rect_Type5 h_Oadd h_Osub h_Omul h_Odiv h_Odivu h_Omod h_Omodu h_Oand h_Oor h_Oxor h_Oshl h_Oshr h_Oshru h_Ocmp h_Ocmpu h_Oaddpi h_Oaddip h_Osubpi h_Osubpp h_Ocmpp x_13425 x_13424 x_13423 = function
 464 | Oadd (sz, sg) -> h_Oadd sz sg
 465 | Osub (sz, sg) -> h_Osub sz sg
 466 | Omul (sz, sg) -> h_Omul sz sg
 467 | Odiv sz -> h_Odiv sz
 468 | Odivu sz -> h_Odivu sz
 469 | Omod sz -> h_Omod sz
 470 | Omodu sz -> h_Omodu sz
 471 | Oand (sz, sg) -> h_Oand sz sg
 472 | Oor (sz, sg) -> h_Oor sz sg
 473 | Oxor (sz, sg) -> h_Oxor sz sg
 474 | Oshl (sz, sg) -> h_Oshl sz sg
 475 | Oshr (sz, sg) -> h_Oshr sz sg
 476 | Oshru (sz, sg) -> h_Oshru sz sg
 477 | Ocmp (sz, sg, sg', x_13427) -> h_Ocmp sz sg sg' x_13427
 478 | Ocmpu (sz, sg', x_13428) -> h_Ocmpu sz sg' x_13428
 479 | Oaddpi sz -> h_Oaddpi sz
 480 | Oaddip sz -> h_Oaddip sz
 481 | Osubpi sz -> h_Osubpi sz
 482 | Osubpp sz -> h_Osubpp sz
 483 | Ocmpp (sg', x_13429) -> h_Ocmpp sg' x_13429
 484
 485 (** val binary_operation_rect_Type3 :
 486     (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness
 487     -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> 'a1)
 488     -> (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) -> (AST.intsize -> 'a1)
 489     -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize ->
 490     AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) ->
 491     (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness
 492     -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize ->
 493     AST.signedness -> AST.signedness -> Integers.comparison -> 'a1) ->
 494     (AST.intsize -> AST.signedness -> Integers.comparison -> 'a1) ->
 495     (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) ->
 496     (AST.intsize -> 'a1) -> (AST.signedness -> Integers.comparison -> 'a1) ->
 497     AST.typ -> AST.typ -> AST.typ -> binary_operation -> 'a1 **)
 498 let rec binary_operation_rect_Type3 h_Oadd h_Osub h_Omul h_Odiv h_Odivu h_Omod h_Omodu h_Oand h_Oor h_Oxor h_Oshl h_Oshr h_Oshru h_Ocmp h_Ocmpu h_Oaddpi h_Oaddip h_Osubpi h_Osubpp h_Ocmpp x_13452 x_13451 x_13450 = function
 499 | Oadd (sz, sg) -> h_Oadd sz sg
 500 | Osub (sz, sg) -> h_Osub sz sg
 501 | Omul (sz, sg) -> h_Omul sz sg
 502 | Odiv sz -> h_Odiv sz
 503 | Odivu sz -> h_Odivu sz
 504 | Omod sz -> h_Omod sz
 505 | Omodu sz -> h_Omodu sz
 506 | Oand (sz, sg) -> h_Oand sz sg
 507 | Oor (sz, sg) -> h_Oor sz sg
 508 | Oxor (sz, sg) -> h_Oxor sz sg
 509 | Oshl (sz, sg) -> h_Oshl sz sg
 510 | Oshr (sz, sg) -> h_Oshr sz sg
 511 | Oshru (sz, sg) -> h_Oshru sz sg
 512 | Ocmp (sz, sg, sg', x_13454) -> h_Ocmp sz sg sg' x_13454
 513 | Ocmpu (sz, sg', x_13455) -> h_Ocmpu sz sg' x_13455
 514 | Oaddpi sz -> h_Oaddpi sz
 515 | Oaddip sz -> h_Oaddip sz
 516 | Osubpi sz -> h_Osubpi sz
 517 | Osubpp sz -> h_Osubpp sz
 518 | Ocmpp (sg', x_13456) -> h_Ocmpp sg' x_13456
 519
 520 (** val binary_operation_rect_Type2 :
 521     (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness
 522     -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> 'a1)
 523     -> (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) -> (AST.intsize -> 'a1)
 524     -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize ->
 525     AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) ->
 526     (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness
 527     -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize ->
 528     AST.signedness -> AST.signedness -> Integers.comparison -> 'a1) ->
 529     (AST.intsize -> AST.signedness -> Integers.comparison -> 'a1) ->
 530     (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) ->
 531     (AST.intsize -> 'a1) -> (AST.signedness -> Integers.comparison -> 'a1) ->
 532     AST.typ -> AST.typ -> AST.typ -> binary_operation -> 'a1 **)
 533 let rec binary_operation_rect_Type2 h_Oadd h_Osub h_Omul h_Odiv h_Odivu h_Omod h_Omodu h_Oand h_Oor h_Oxor h_Oshl h_Oshr h_Oshru h_Ocmp h_Ocmpu h_Oaddpi h_Oaddip h_Osubpi h_Osubpp h_Ocmpp x_13479 x_13478 x_13477 = function
 534 | Oadd (sz, sg) -> h_Oadd sz sg
 535 | Osub (sz, sg) -> h_Osub sz sg
 536 | Omul (sz, sg) -> h_Omul sz sg
 537 | Odiv sz -> h_Odiv sz
 538 | Odivu sz -> h_Odivu sz
 539 | Omod sz -> h_Omod sz
 540 | Omodu sz -> h_Omodu sz
 541 | Oand (sz, sg) -> h_Oand sz sg
 542 | Oor (sz, sg) -> h_Oor sz sg
 543 | Oxor (sz, sg) -> h_Oxor sz sg
 544 | Oshl (sz, sg) -> h_Oshl sz sg
 545 | Oshr (sz, sg) -> h_Oshr sz sg
 546 | Oshru (sz, sg) -> h_Oshru sz sg
 547 | Ocmp (sz, sg, sg', x_13481) -> h_Ocmp sz sg sg' x_13481
 548 | Ocmpu (sz, sg', x_13482) -> h_Ocmpu sz sg' x_13482
 549 | Oaddpi sz -> h_Oaddpi sz
 550 | Oaddip sz -> h_Oaddip sz
 551 | Osubpi sz -> h_Osubpi sz
 552 | Osubpp sz -> h_Osubpp sz
 553 | Ocmpp (sg', x_13483) -> h_Ocmpp sg' x_13483
 554
 555 (** val binary_operation_rect_Type1 :
 556     (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness
 557     -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> 'a1)
 558     -> (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) -> (AST.intsize -> 'a1)
 559     -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize ->
 560     AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) ->
 561     (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness
 562     -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize ->
 563     AST.signedness -> AST.signedness -> Integers.comparison -> 'a1) ->
 564     (AST.intsize -> AST.signedness -> Integers.comparison -> 'a1) ->
 565     (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) ->
 566     (AST.intsize -> 'a1) -> (AST.signedness -> Integers.comparison -> 'a1) ->
 567     AST.typ -> AST.typ -> AST.typ -> binary_operation -> 'a1 **)
 568 let rec binary_operation_rect_Type1 h_Oadd h_Osub h_Omul h_Odiv h_Odivu h_Omod h_Omodu h_Oand h_Oor h_Oxor h_Oshl h_Oshr h_Oshru h_Ocmp h_Ocmpu h_Oaddpi h_Oaddip h_Osubpi h_Osubpp h_Ocmpp x_13506 x_13505 x_13504 = function
 569 | Oadd (sz, sg) -> h_Oadd sz sg
 570 | Osub (sz, sg) -> h_Osub sz sg
 571 | Omul (sz, sg) -> h_Omul sz sg
 572 | Odiv sz -> h_Odiv sz
 573 | Odivu sz -> h_Odivu sz
 574 | Omod sz -> h_Omod sz
 575 | Omodu sz -> h_Omodu sz
 576 | Oand (sz, sg) -> h_Oand sz sg
 577 | Oor (sz, sg) -> h_Oor sz sg
 578 | Oxor (sz, sg) -> h_Oxor sz sg
 579 | Oshl (sz, sg) -> h_Oshl sz sg
 580 | Oshr (sz, sg) -> h_Oshr sz sg
 581 | Oshru (sz, sg) -> h_Oshru sz sg
 582 | Ocmp (sz, sg, sg', x_13508) -> h_Ocmp sz sg sg' x_13508
 583 | Ocmpu (sz, sg', x_13509) -> h_Ocmpu sz sg' x_13509
 584 | Oaddpi sz -> h_Oaddpi sz
 585 | Oaddip sz -> h_Oaddip sz
 586 | Osubpi sz -> h_Osubpi sz
 587 | Osubpp sz -> h_Osubpp sz
 588 | Ocmpp (sg', x_13510) -> h_Ocmpp sg' x_13510
 589
 590 (** val binary_operation_rect_Type0 :
 591     (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness
 592     -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> 'a1)
 593     -> (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) -> (AST.intsize -> 'a1)
 594     -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize ->
 595     AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) ->
 596     (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness
 597     -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize ->
 598     AST.signedness -> AST.signedness -> Integers.comparison -> 'a1) ->
 599     (AST.intsize -> AST.signedness -> Integers.comparison -> 'a1) ->
 600     (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) ->
 601     (AST.intsize -> 'a1) -> (AST.signedness -> Integers.comparison -> 'a1) ->
 602     AST.typ -> AST.typ -> AST.typ -> binary_operation -> 'a1 **)
 603 let rec binary_operation_rect_Type0 h_Oadd h_Osub h_Omul h_Odiv h_Odivu h_Omod h_Omodu h_Oand h_Oor h_Oxor h_Oshl h_Oshr h_Oshru h_Ocmp h_Ocmpu h_Oaddpi h_Oaddip h_Osubpi h_Osubpp h_Ocmpp x_13533 x_13532 x_13531 = function
 604 | Oadd (sz, sg) -> h_Oadd sz sg
 605 | Osub (sz, sg) -> h_Osub sz sg
 606 | Omul (sz, sg) -> h_Omul sz sg
 607 | Odiv sz -> h_Odiv sz
 608 | Odivu sz -> h_Odivu sz
 609 | Omod sz -> h_Omod sz
 610 | Omodu sz -> h_Omodu sz
 611 | Oand (sz, sg) -> h_Oand sz sg
 612 | Oor (sz, sg) -> h_Oor sz sg
 613 | Oxor (sz, sg) -> h_Oxor sz sg
 614 | Oshl (sz, sg) -> h_Oshl sz sg
 615 | Oshr (sz, sg) -> h_Oshr sz sg
 616 | Oshru (sz, sg) -> h_Oshru sz sg
 617 | Ocmp (sz, sg, sg', x_13535) -> h_Ocmp sz sg sg' x_13535
 618 | Ocmpu (sz, sg', x_13536) -> h_Ocmpu sz sg' x_13536
 619 | Oaddpi sz -> h_Oaddpi sz
 620 | Oaddip sz -> h_Oaddip sz
 621 | Osubpi sz -> h_Osubpi sz
 622 | Osubpp sz -> h_Osubpp sz
 623 | Ocmpp (sg', x_13537) -> h_Ocmpp sg' x_13537
 624
 625 (** val binary_operation_inv_rect_Type4 :
 626     AST.typ -> AST.typ -> AST.typ -> binary_operation -> (AST.intsize ->
 627     AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
 628     AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
 629     AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ ->
 630     __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __ -> __ -> __ -> 'a1) ->
 631     (AST.intsize -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __
 632     -> __ -> __ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __
 633     -> __ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __
 634     -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1)
 635     -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
 636     (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
 637     (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
 638     (AST.intsize -> AST.signedness -> AST.signedness -> Integers.comparison
 639     -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> AST.signedness ->
 640     Integers.comparison -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __
 641     -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __ -> __ -> __ -> 'a1)
 642     -> (AST.intsize -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ ->
 643     __ -> __ -> __ -> 'a1) -> (AST.signedness -> Integers.comparison -> __ ->
 644     __ -> __ -> __ -> 'a1) -> 'a1 **)
 645 let binary_operation_inv_rect_Type4 x1 x2 x3 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 h20 =
 646   let hcut =
 647     binary_operation_rect_Type4 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13
 648       h14 h15 h16 h17 h18 h19 h20 x1 x2 x3 hterm
 649   in
 650   hcut __ __ __ __
 651
 652 (** val binary_operation_inv_rect_Type3 :
 653     AST.typ -> AST.typ -> AST.typ -> binary_operation -> (AST.intsize ->
 654     AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
 655     AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
 656     AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ ->
 657     __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __ -> __ -> __ -> 'a1) ->
 658     (AST.intsize -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __
 659     -> __ -> __ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __
 660     -> __ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __
 661     -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1)
 662     -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
 663     (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
 664     (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
 665     (AST.intsize -> AST.signedness -> AST.signedness -> Integers.comparison
 666     -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> AST.signedness ->
 667     Integers.comparison -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __
 668     -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __ -> __ -> __ -> 'a1)
 669     -> (AST.intsize -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ ->
 670     __ -> __ -> __ -> 'a1) -> (AST.signedness -> Integers.comparison -> __ ->
 671     __ -> __ -> __ -> 'a1) -> 'a1 **)
 672 let binary_operation_inv_rect_Type3 x1 x2 x3 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 h20 =
 673   let hcut =
 674     binary_operation_rect_Type3 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13
 675       h14 h15 h16 h17 h18 h19 h20 x1 x2 x3 hterm
 676   in
 677   hcut __ __ __ __
 678
 679 (** val binary_operation_inv_rect_Type2 :
 680     AST.typ -> AST.typ -> AST.typ -> binary_operation -> (AST.intsize ->
 681     AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
 682     AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
 683     AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ ->
 684     __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __ -> __ -> __ -> 'a1) ->
 685     (AST.intsize -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __
 686     -> __ -> __ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __
 687     -> __ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __
 688     -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1)
 689     -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
 690     (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
 691     (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
 692     (AST.intsize -> AST.signedness -> AST.signedness -> Integers.comparison
 693     -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> AST.signedness ->
 694     Integers.comparison -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __
 695     -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __ -> __ -> __ -> 'a1)
 696     -> (AST.intsize -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ ->
 697     __ -> __ -> __ -> 'a1) -> (AST.signedness -> Integers.comparison -> __ ->
 698     __ -> __ -> __ -> 'a1) -> 'a1 **)
 699 let binary_operation_inv_rect_Type2 x1 x2 x3 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 h20 =
 700   let hcut =
 701     binary_operation_rect_Type2 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13
 702       h14 h15 h16 h17 h18 h19 h20 x1 x2 x3 hterm
 703   in
 704   hcut __ __ __ __
 705
 706 (** val binary_operation_inv_rect_Type1 :
 707     AST.typ -> AST.typ -> AST.typ -> binary_operation -> (AST.intsize ->
 708     AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
 709     AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
 710     AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ ->
 711     __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __ -> __ -> __ -> 'a1) ->
 712     (AST.intsize -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __
 713     -> __ -> __ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __
 714     -> __ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __
 715     -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1)
 716     -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
 717     (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
 718     (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
 719     (AST.intsize -> AST.signedness -> AST.signedness -> Integers.comparison
 720     -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> AST.signedness ->
 721     Integers.comparison -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __
 722     -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __ -> __ -> __ -> 'a1)
 723     -> (AST.intsize -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ ->
 724     __ -> __ -> __ -> 'a1) -> (AST.signedness -> Integers.comparison -> __ ->
 725     __ -> __ -> __ -> 'a1) -> 'a1 **)
 726 let binary_operation_inv_rect_Type1 x1 x2 x3 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 h20 =
 727   let hcut =
 728     binary_operation_rect_Type1 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13
 729       h14 h15 h16 h17 h18 h19 h20 x1 x2 x3 hterm
 730   in
 731   hcut __ __ __ __
 732
 733 (** val binary_operation_inv_rect_Type0 :
 734     AST.typ -> AST.typ -> AST.typ -> binary_operation -> (AST.intsize ->
 735     AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
 736     AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
 737     AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ ->
 738     __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __ -> __ -> __ -> 'a1) ->
 739     (AST.intsize -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __
 740     -> __ -> __ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __
 741     -> __ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __
 742     -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1)
 743     -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
 744     (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
 745     (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
 746     (AST.intsize -> AST.signedness -> AST.signedness -> Integers.comparison
 747     -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> AST.signedness ->
 748     Integers.comparison -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __
 749     -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __ -> __ -> __ -> 'a1)
 750     -> (AST.intsize -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ ->
 751     __ -> __ -> __ -> 'a1) -> (AST.signedness -> Integers.comparison -> __ ->
 752     __ -> __ -> __ -> 'a1) -> 'a1 **)
 753 let binary_operation_inv_rect_Type0 x1 x2 x3 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 h20 =
 754   let hcut =
 755     binary_operation_rect_Type0 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13
 756       h14 h15 h16 h17 h18 h19 h20 x1 x2 x3 hterm
 757   in
 758   hcut __ __ __ __
 759
 760 (** val binary_operation_discr :
 761     AST.typ -> AST.typ -> AST.typ -> binary_operation -> binary_operation ->
 762     __ **)
 763 let binary_operation_discr a1 a2 a3 x y =
 764   Logic.eq_rect_Type2 x
 765     (match x with
 766      | Oadd (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
 767      | Osub (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
 768      | Omul (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
 769      | Odiv a0 -> Obj.magic (fun _ dH -> dH __)
 770      | Odivu a0 -> Obj.magic (fun _ dH -> dH __)
 771      | Omod a0 -> Obj.magic (fun _ dH -> dH __)
 772      | Omodu a0 -> Obj.magic (fun _ dH -> dH __)
 773      | Oand (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
 774      | Oor (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
 775      | Oxor (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
 776      | Oshl (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
 777      | Oshr (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
 778      | Oshru (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
 779      | Ocmp (a0, a10, a20, a30) -> Obj.magic (fun _ dH -> dH __ __ __ __)
 780      | Ocmpu (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __)
 781      | Oaddpi a0 -> Obj.magic (fun _ dH -> dH __)
 782      | Oaddip a0 -> Obj.magic (fun _ dH -> dH __)
 783      | Osubpi a0 -> Obj.magic (fun _ dH -> dH __)
 784      | Osubpp a0 -> Obj.magic (fun _ dH -> dH __)
 785      | Ocmpp (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)) y
 786
 787 (** val binary_operation_jmdiscr :
 788     AST.typ -> AST.typ -> AST.typ -> binary_operation -> binary_operation ->
 789     __ **)
 790 let binary_operation_jmdiscr a1 a2 a3 x y =
 791   Logic.eq_rect_Type2 x
 792     (match x with
 793      | Oadd (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
 794      | Osub (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
 795      | Omul (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
 796      | Odiv a0 -> Obj.magic (fun _ dH -> dH __)
 797      | Odivu a0 -> Obj.magic (fun _ dH -> dH __)
 798      | Omod a0 -> Obj.magic (fun _ dH -> dH __)
 799      | Omodu a0 -> Obj.magic (fun _ dH -> dH __)
 800      | Oand (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
 801      | Oor (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
 802      | Oxor (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
 803      | Oshl (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
 804      | Oshr (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
 805      | Oshru (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
 806      | Ocmp (a0, a10, a20, a30) -> Obj.magic (fun _ dH -> dH __ __ __ __)
 807      | Ocmpu (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __)
 808      | Oaddpi a0 -> Obj.magic (fun _ dH -> dH __)
 809      | Oaddip a0 -> Obj.magic (fun _ dH -> dH __)
 810      | Osubpi a0 -> Obj.magic (fun _ dH -> dH __)
 811      | Osubpp a0 -> Obj.magic (fun _ dH -> dH __)
 812      | Ocmpp (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)) y
 813
 814 (** val eval_constant :
 815     AST.typ -> (AST.ident -> Pointers.block Types.option) -> Pointers.block
 816     -> constant -> Values.val0 Types.option **)
 817 let eval_constant t find_symbol sp = function
 818 | Ointconst (sz, sg, n) -> Types.Some (Values.Vint (sz, n))
 819 | Oaddrsymbol (s, ofs) ->
 820   (match find_symbol s with
 821    | Types.None -> Types.None
 822    | Types.Some b ->
 823      Types.Some (Values.Vptr { Pointers.pblock = b; Pointers.poff =
 824        (Pointers.shift_offset (AST.bitsize_of_intsize AST.I16)
 825          Pointers.zero_offset (AST.repr AST.I16 ofs)) }))
 826 | Oaddrstack ofs ->
 827   Types.Some (Values.Vptr { Pointers.pblock = sp; Pointers.poff =
 828     (Pointers.shift_offset (AST.bitsize_of_intsize AST.I16)
 829       Pointers.zero_offset (AST.repr AST.I16 ofs)) })
 830
 831 (** val eval_unop :
 832     AST.typ -> AST.typ -> unary_operation -> Values.val0 -> Values.val0
 833     Types.option **)
 834 let eval_unop t t' op arg =
 835   match op with
 836   | Ocastint (sz, sg, sz', sg') ->
 837     (match sg with
 838      | AST.Signed -> Types.Some (Values.sign_ext sz' arg)
 839      | AST.Unsigned -> Types.Some (Values.zero_ext sz' arg))
 840   | Onegint (sz, sg) ->
 841     (match arg with
 842      | Values.Vundef -> Types.None
 843      | Values.Vint (sz1, n1) ->
 844        Types.Some (Values.Vint (sz1,
 845          (Arithmetic.two_complement_negation (AST.bitsize_of_intsize sz1) n1)))
 846      | Values.Vnull -> Types.None
 847      | Values.Vptr x -> Types.None)
 848   | Onotbool (t0, sz, sg) ->
 849     (match arg with
 850      | Values.Vundef -> Types.None
 851      | Values.Vint (sz1, n1) ->
 852        Types.Some (Values.Vint (sz,
 853          (match BitVector.eq_bv (AST.bitsize_of_intsize sz1) n1
 854                   (BitVector.zero (AST.bitsize_of_intsize sz1)) with
 855           | Bool.True -> AST.repr sz (Nat.S Nat.O)
 856           | Bool.False -> BitVector.zero (AST.bitsize_of_intsize sz))))
 857      | Values.Vnull ->
 858        Types.Some (Values.Vint (sz, (AST.repr sz (Nat.S Nat.O))))
 859      | Values.Vptr x0 ->
 860        Types.Some (Values.Vint (sz,
 861          (BitVector.zero (AST.bitsize_of_intsize sz)))))
 862   | Onotint (sz, sg) ->
 863     (match arg with
 864      | Values.Vundef -> Types.None
 865      | Values.Vint (sz1, n1) ->
 866        Types.Some (Values.Vint (sz1,
 867          (BitVector.exclusive_disjunction_bv (AST.bitsize_of_intsize sz1) n1
 868            (Values.mone sz1))))
 869      | Values.Vnull -> Types.None
 870      | Values.Vptr x -> Types.None)
 871   | Oid t0 -> Types.Some arg
 872   | Optrofint (sz, sg) ->
 873     (match arg with
 874      | Values.Vundef -> Types.None
 875      | Values.Vint (sz1, n1) ->
 876        (match BitVector.eq_bv (AST.bitsize_of_intsize sz1) n1
 877                 (BitVector.zero (AST.bitsize_of_intsize sz1)) with
 878         | Bool.True -> Types.Some Values.Vnull
 879         | Bool.False -> Types.None)
 880      | Values.Vnull -> Types.None
 881      | Values.Vptr x -> Types.None)
 882   | Ointofptr (sz, sg) ->
 883     (match arg with
 884      | Values.Vundef -> Types.None
 885      | Values.Vint (x, x0) -> Types.None
 886      | Values.Vnull ->
 887        Types.Some (Values.Vint (sz,
 888          (BitVector.zero (AST.bitsize_of_intsize sz))))
 889      | Values.Vptr x -> Types.None)
 890
 891 (** val eval_compare_mismatch :
 892     Integers.comparison -> Values.val0 Types.option **)
 893 let eval_compare_mismatch = function
 894 | Integers.Ceq -> Types.Some Values.vfalse
 895 | Integers.Cne -> Types.Some Values.vtrue
 896 | Integers.Clt -> Types.None
 897 | Integers.Cle -> Types.None
 898 | Integers.Cgt -> Types.None
 899 | Integers.Cge -> Types.None
 900
 901 (** val ev_add : Values.val0 -> Values.val0 -> Values.val0 Types.option **)
 902 let ev_add v1 v2 =
 903   match v1 with
 904   | Values.Vundef -> Types.None
 905   | Values.Vint (sz1, n1) ->
 906     (match v2 with
 907      | Values.Vundef -> Types.None
 908      | Values.Vint (sz2, n2) ->
 909        AST.intsize_eq_elim sz1 sz2 n1 (fun n10 -> Types.Some (Values.Vint
 910          (sz2, (Arithmetic.addition_n (AST.bitsize_of_intsize sz2) n10 n2))))
 911          Types.None
 912      | Values.Vnull -> Types.None
 913      | Values.Vptr x -> Types.None)
 914   | Values.Vnull -> Types.None
 915   | Values.Vptr x -> Types.None
 916
 917 (** val ev_sub : Values.val0 -> Values.val0 -> Values.val0 Types.option **)
 918 let ev_sub v1 v2 =
 919   match v1 with
 920   | Values.Vundef -> Types.None
 921   | Values.Vint (sz1, n1) ->
 922     (match v2 with
 923      | Values.Vundef -> Types.None
 924      | Values.Vint (sz2, n2) ->
 925        AST.intsize_eq_elim sz1 sz2 n1 (fun n10 -> Types.Some (Values.Vint
 926          (sz2,
 927          (Arithmetic.subtraction (AST.bitsize_of_intsize sz2) n10 n2))))
 928          Types.None
 929      | Values.Vnull -> Types.None
 930      | Values.Vptr x -> Types.None)
 931   | Values.Vnull -> Types.None
 932   | Values.Vptr x -> Types.None
 933
 934 (** val ev_addpi : Values.val0 -> Values.val0 -> Values.val0 Types.option **)
 935 let ev_addpi v1 v2 =
 936   match v1 with
 937   | Values.Vundef -> Types.None
 938   | Values.Vint (x, x0) -> Types.None
 939   | Values.Vnull ->
 940     (match v2 with
 941      | Values.Vundef -> Types.None
 942      | Values.Vint (sz2, n2) ->
 943        (match BitVector.eq_bv (AST.bitsize_of_intsize sz2) n2
 944                 (BitVector.zero (AST.bitsize_of_intsize sz2)) with
 945         | Bool.True -> Types.Some Values.Vnull
 946         | Bool.False -> Types.None)
 947      | Values.Vnull -> Types.None
 948      | Values.Vptr x -> Types.None)
 949   | Values.Vptr ptr1 ->
 950     (match v2 with
 951      | Values.Vundef -> Types.None
 952      | Values.Vint (sz2, n2) ->
 953        Types.Some (Values.Vptr
 954          (Pointers.shift_pointer (AST.bitsize_of_intsize sz2) ptr1 n2))
 955      | Values.Vnull -> Types.None
 956      | Values.Vptr x -> Types.None)
 957
 958 (** val ev_subpi : Values.val0 -> Values.val0 -> Values.val0 Types.option **)
 959 let ev_subpi v1 v2 =
 960   match v1 with
 961   | Values.Vundef -> Types.None
 962   | Values.Vint (x, x0) -> Types.None
 963   | Values.Vnull ->
 964     (match v2 with
 965      | Values.Vundef -> Types.None
 966      | Values.Vint (sz2, n2) ->
 967        (match BitVector.eq_bv (AST.bitsize_of_intsize sz2) n2
 968                 (BitVector.zero (AST.bitsize_of_intsize sz2)) with
 969         | Bool.True -> Types.Some Values.Vnull
 970         | Bool.False -> Types.None)
 971      | Values.Vnull -> Types.None
 972      | Values.Vptr x -> Types.None)
 973   | Values.Vptr ptr1 ->
 974     (match v2 with
 975      | Values.Vundef -> Types.None
 976      | Values.Vint (sz2, n2) ->
 977        Types.Some (Values.Vptr
 978          (Pointers.neg_shift_pointer (AST.bitsize_of_intsize sz2) ptr1 n2))
 979      | Values.Vnull -> Types.None
 980      | Values.Vptr x -> Types.None)
 981
 982 (** val ev_subpp :
 983     AST.intsize -> Values.val0 -> Values.val0 -> Values.val0 Types.option **)
 984 let ev_subpp sz v1 v2 =
 985   match v1 with
 986   | Values.Vundef -> Types.None
 987   | Values.Vint (x, x0) -> Types.None
 988   | Values.Vnull ->
 989     (match v2 with
 990      | Values.Vundef -> Types.None
 991      | Values.Vint (x, x0) -> Types.None
 992      | Values.Vnull ->
 993        Types.Some (Values.Vint (sz,
 994          (BitVector.zero (AST.bitsize_of_intsize sz))))
 995      | Values.Vptr x -> Types.None)
 996   | Values.Vptr ptr1 ->
 997     (match v2 with
 998      | Values.Vundef -> Types.None
 999      | Values.Vint (x, x0) -> Types.None
1000      | Values.Vnull -> Types.None
1001      | Values.Vptr ptr2 ->
1002        (match Pointers.eq_block ptr1.Pointers.pblock ptr2.Pointers.pblock with
1003         | Bool.True ->
1004           Types.Some (Values.Vint (sz,
1005             (Pointers.sub_offset (AST.bitsize_of_intsize sz)
1006               ptr1.Pointers.poff ptr2.Pointers.poff)))
1007         | Bool.False -> Types.None))
1008
1009 (** val ev_mul : Values.val0 -> Values.val0 -> Values.val0 Types.option **)
1010 let ev_mul v1 v2 =
1011   match v1 with
1012   | Values.Vundef -> Types.None
1013   | Values.Vint (sz1, n1) ->
1014     (match v2 with
1015      | Values.Vundef -> Types.None
1016      | Values.Vint (sz2, n2) ->
1017        AST.intsize_eq_elim sz1 sz2 n1 (fun n10 -> Types.Some (Values.Vint
1018          (sz2,
1019          (Arithmetic.short_multiplication (AST.bitsize_of_intsize sz2) n10
1020            n2)))) Types.None
1021      | Values.Vnull -> Types.None
1022      | Values.Vptr x -> Types.None)
1023   | Values.Vnull -> Types.None
1024   | Values.Vptr x -> Types.None
1025
1026 (** val ev_divs : Values.val0 -> Values.val0 -> Values.val0 Types.option **)
1027 let ev_divs v1 v2 =
1028   match v1 with
1029   | Values.Vundef -> Types.None
1030   | Values.Vint (sz1, n1) ->
1031     (match v2 with
1032      | Values.Vundef -> Types.None
1033      | Values.Vint (sz2, n2) ->
1034        AST.intsize_eq_elim sz1 sz2 n1 (fun n10 ->
1035          Types.option_map (fun x -> Values.Vint (sz2, x))
1036            (Arithmetic.division_s (AST.bitsize_of_intsize sz2) n10 n2))
1037          Types.None
1038      | Values.Vnull -> Types.None
1039      | Values.Vptr x -> Types.None)
1040   | Values.Vnull -> Types.None
1041   | Values.Vptr x -> Types.None
1042
1043 (** val ev_mods : Values.val0 -> Values.val0 -> Values.val0 Types.option **)
1044 let ev_mods v1 v2 =
1045   match v1 with
1046   | Values.Vundef -> Types.None
1047   | Values.Vint (sz1, n1) ->
1048     (match v2 with
1049      | Values.Vundef -> Types.None
1050      | Values.Vint (sz2, n2) ->
1051        AST.intsize_eq_elim sz1 sz2 n1 (fun n10 ->
1052          Types.option_map (fun x -> Values.Vint (sz2, x))
1053            (Arithmetic.modulus_s (AST.bitsize_of_intsize sz2) n10 n2))
1054          Types.None
1055      | Values.Vnull -> Types.None
1056      | Values.Vptr x -> Types.None)
1057   | Values.Vnull -> Types.None
1058   | Values.Vptr x -> Types.None
1059
1060 (** val ev_divu : Values.val0 -> Values.val0 -> Values.val0 Types.option **)
1061 let ev_divu v1 v2 =
1062   match v1 with
1063   | Values.Vundef -> Types.None
1064   | Values.Vint (sz1, n1) ->
1065     (match v2 with
1066      | Values.Vundef -> Types.None
1067      | Values.Vint (sz2, n2) ->
1068        AST.intsize_eq_elim sz1 sz2 n1 (fun n10 ->
1069          Types.option_map (fun x -> Values.Vint (sz2, x))
1070            (Arithmetic.division_u
1071              (Nat.plus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1072                Nat.O)))))))
1073                (Nat.times (AST.pred_size_intsize sz2) (Nat.S (Nat.S (Nat.S
1074                  (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))) n10 n2))
1075          Types.None
1076      | Values.Vnull -> Types.None
1077      | Values.Vptr x -> Types.None)
1078   | Values.Vnull -> Types.None
1079   | Values.Vptr x -> Types.None
1080
1081 (** val ev_modu : Values.val0 -> Values.val0 -> Values.val0 Types.option **)
1082 let ev_modu v1 v2 =
1083   match v1 with
1084   | Values.Vundef -> Types.None
1085   | Values.Vint (sz1, n1) ->
1086     (match v2 with
1087      | Values.Vundef -> Types.None
1088      | Values.Vint (sz2, n2) ->
1089        AST.intsize_eq_elim sz1 sz2 n1 (fun n10 ->
1090          Types.option_map (fun x -> Values.Vint (sz2, x))
1091            (Arithmetic.modulus_u
1092              (Nat.plus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1093                Nat.O)))))))
1094                (Nat.times (AST.pred_size_intsize sz2) (Nat.S (Nat.S (Nat.S
1095                  (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))) n10 n2))
1096          Types.None
1097      | Values.Vnull -> Types.None
1098      | Values.Vptr x -> Types.None)
1099   | Values.Vnull -> Types.None
1100   | Values.Vptr x -> Types.None
1101
1102 (** val ev_and : Values.val0 -> Values.val0 -> Values.val0 Types.option **)
1103 let ev_and v1 v2 =
1104   match v1 with
1105   | Values.Vundef -> Types.None
1106   | Values.Vint (sz1, n1) ->
1107     (match v2 with
1108      | Values.Vundef -> Types.None
1109      | Values.Vint (sz2, n2) ->
1110        AST.intsize_eq_elim sz1 sz2 n1 (fun n10 -> Types.Some (Values.Vint
1111          (sz2,
1112          (BitVector.conjunction_bv (AST.bitsize_of_intsize sz2) n10 n2))))
1113          Types.None
1114      | Values.Vnull -> Types.None
1115      | Values.Vptr x -> Types.None)
1116   | Values.Vnull -> Types.None
1117   | Values.Vptr x -> Types.None
1118
1119 (** val ev_or : Values.val0 -> Values.val0 -> Values.val0 Types.option **)
1120 let ev_or v1 v2 =
1121   match v1 with
1122   | Values.Vundef -> Types.None
1123   | Values.Vint (sz1, n1) ->
1124     (match v2 with
1125      | Values.Vundef -> Types.None
1126      | Values.Vint (sz2, n2) ->
1127        AST.intsize_eq_elim sz1 sz2 n1 (fun n10 -> Types.Some (Values.Vint
1128          (sz2,
1129          (BitVector.inclusive_disjunction_bv (AST.bitsize_of_intsize sz2) n10
1130            n2)))) Types.None
1131      | Values.Vnull -> Types.None
1132      | Values.Vptr x -> Types.None)
1133   | Values.Vnull -> Types.None
1134   | Values.Vptr x -> Types.None
1135
1136 (** val ev_xor : Values.val0 -> Values.val0 -> Values.val0 Types.option **)
1137 let ev_xor v1 v2 =
1138   match v1 with
1139   | Values.Vundef -> Types.None
1140   | Values.Vint (sz1, n1) ->
1141     (match v2 with
1142      | Values.Vundef -> Types.None
1143      | Values.Vint (sz2, n2) ->
1144        AST.intsize_eq_elim sz1 sz2 n1 (fun n10 -> Types.Some (Values.Vint
1145          (sz2,
1146          (BitVector.exclusive_disjunction_bv (AST.bitsize_of_intsize sz2) n10
1147            n2)))) Types.None
1148      | Values.Vnull -> Types.None
1149      | Values.Vptr x -> Types.None)
1150   | Values.Vnull -> Types.None
1151   | Values.Vptr x -> Types.None
1152
1153 (** val ev_shl : Values.val0 -> Values.val0 -> Values.val0 Types.option **)
1154 let ev_shl v1 v2 =
1155   match v1 with
1156   | Values.Vundef -> Types.None
1157   | Values.Vint (sz1, n1) ->
1158     (match v2 with
1159      | Values.Vundef -> Types.None
1160      | Values.Vint (sz2, n2) ->
1161        (match Arithmetic.lt_u (AST.bitsize_of_intsize sz2) n2
1162                 (Arithmetic.bitvector_of_nat (AST.bitsize_of_intsize sz2)
1163                   (AST.bitsize_of_intsize sz1)) with
1164         | Bool.True ->
1165           Types.Some (Values.Vint (sz1,
1166             (Vector.shift_left (AST.bitsize_of_intsize sz1)
1167               (Arithmetic.nat_of_bitvector (AST.bitsize_of_intsize sz2) n2)
1168               n1 Bool.False)))
1169         | Bool.False -> Types.None)
1170      | Values.Vnull -> Types.None
1171      | Values.Vptr x -> Types.None)
1172   | Values.Vnull -> Types.None
1173   | Values.Vptr x -> Types.None
1174
1175 (** val ev_shr : Values.val0 -> Values.val0 -> Values.val0 Types.option **)
1176 let ev_shr v1 v2 =
1177   match v1 with
1178   | Values.Vundef -> Types.None
1179   | Values.Vint (sz1, n1) ->
1180     (match v2 with
1181      | Values.Vundef -> Types.None
1182      | Values.Vint (sz2, n2) ->
1183        (match Arithmetic.lt_u (AST.bitsize_of_intsize sz2) n2
1184                 (Arithmetic.bitvector_of_nat (AST.bitsize_of_intsize sz2)
1185                   (AST.bitsize_of_intsize sz1)) with
1186         | Bool.True ->
1187           Types.Some (Values.Vint (sz1,
1188             (Vector.shift_right
1189               (Nat.plus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1190                 Nat.O)))))))
1191                 (Nat.times (AST.pred_size_intsize sz1) (Nat.S (Nat.S (Nat.S
1192                   (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))))
1193               (Arithmetic.nat_of_bitvector (AST.bitsize_of_intsize sz2) n2)
1194               n1
1195               (Vector.head'
1196                 (Nat.plus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1197                   Nat.O)))))))
1198                   (Nat.times (AST.pred_size_intsize sz1) (Nat.S (Nat.S (Nat.S
1199                     (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))) n1))))
1200         | Bool.False -> Types.None)
1201      | Values.Vnull -> Types.None
1202      | Values.Vptr x -> Types.None)
1203   | Values.Vnull -> Types.None
1204   | Values.Vptr x -> Types.None
1205
1206 (** val ev_shru : Values.val0 -> Values.val0 -> Values.val0 Types.option **)
1207 let ev_shru v1 v2 =
1208   match v1 with
1209   | Values.Vundef -> Types.None
1210   | Values.Vint (sz1, n1) ->
1211     (match v2 with
1212      | Values.Vundef -> Types.None
1213      | Values.Vint (sz2, n2) ->
1214        (match Arithmetic.lt_u (AST.bitsize_of_intsize sz2) n2
1215                 (Arithmetic.bitvector_of_nat (AST.bitsize_of_intsize sz2)
1216                   (AST.bitsize_of_intsize sz1)) with
1217         | Bool.True ->
1218           Types.Some (Values.Vint (sz1,
1219             (Vector.shift_right
1220               (Nat.plus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1221                 Nat.O)))))))
1222                 (Nat.times (AST.pred_size_intsize sz1) (Nat.S (Nat.S (Nat.S
1223                   (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))))
1224               (Arithmetic.nat_of_bitvector (AST.bitsize_of_intsize sz2) n2)
1225               n1 Bool.False)))
1226         | Bool.False -> Types.None)
1227      | Values.Vnull -> Types.None
1228      | Values.Vptr x -> Types.None)
1229   | Values.Vnull -> Types.None
1230   | Values.Vptr x -> Types.None
1231
1232 (** val fEtrue : Values.val0 **)
1233 let fEtrue =
1234   Values.Vint (AST.I8, (AST.repr AST.I8 (Nat.S Nat.O)))
1235
1236 (** val fEfalse : Values.val0 **)
1237 let fEfalse =
1238   Values.Vint (AST.I8, (AST.repr AST.I8 Nat.O))
1239
1240 (** val fE_of_bool : Bool.bool -> Values.val0 **)
1241 let fE_of_bool = function
1242 | Bool.True -> fEtrue
1243 | Bool.False -> fEfalse
1244
1245 (** val ev_cmp_match : Integers.comparison -> Values.val0 Types.option **)
1246 let ev_cmp_match = function
1247 | Integers.Ceq -> Types.Some fEtrue
1248 | Integers.Cne -> Types.Some fEfalse
1249 | Integers.Clt -> Types.None
1250 | Integers.Cle -> Types.None
1251 | Integers.Cgt -> Types.None
1252 | Integers.Cge -> Types.None
1253
1254 (** val ev_cmp_mismatch : Integers.comparison -> Values.val0 Types.option **)
1255 let ev_cmp_mismatch = function
1256 | Integers.Ceq -> Types.Some fEfalse
1257 | Integers.Cne -> Types.Some fEtrue
1258 | Integers.Clt -> Types.None
1259 | Integers.Cle -> Types.None
1260 | Integers.Cgt -> Types.None
1261 | Integers.Cge -> Types.None
1262
1263 (** val ev_cmp :
1264     Integers.comparison -> Values.val0 -> Values.val0 -> Values.val0
1265     Types.option **)
1266 let ev_cmp c v1 v2 =
1267   match v1 with
1268   | Values.Vundef -> Types.None
1269   | Values.Vint (sz1, n1) ->
1270     (match v2 with
1271      | Values.Vundef -> Types.None
1272      | Values.Vint (sz2, n2) ->
1273        AST.intsize_eq_elim sz1 sz2 n1 (fun n10 -> Types.Some
1274          (fE_of_bool (Values.cmp_int (AST.bitsize_of_intsize sz2) c n10 n2)))
1275          Types.None
1276      | Values.Vnull -> Types.None
1277      | Values.Vptr x -> Types.None)
1278   | Values.Vnull -> Types.None
1279   | Values.Vptr x -> Types.None
1280
1281 (** val ev_cmpp :
1282     GenMem.mem -> Integers.comparison -> Values.val0 -> Values.val0 ->
1283     Values.val0 Types.option **)
1284 let ev_cmpp m c v1 v2 =
1285   match v1 with
1286   | Values.Vundef -> Types.None
1287   | Values.Vint (x, x0) -> Types.None
1288   | Values.Vnull ->
1289     (match v2 with
1290      | Values.Vundef -> Types.None
1291      | Values.Vint (x, x0) -> Types.None
1292      | Values.Vnull -> ev_cmp_match c
1293      | Values.Vptr x -> ev_cmp_mismatch c)
1294   | Values.Vptr ptr1 ->
1295     (match v2 with
1296      | Values.Vundef -> Types.None
1297      | Values.Vint (x, x0) -> Types.None
1298      | Values.Vnull -> ev_cmp_mismatch c
1299      | Values.Vptr ptr2 ->
1300        (match Bool.andb (FrontEndMem.valid_pointer m ptr1)
1301                 (FrontEndMem.valid_pointer m ptr2) with
1302         | Bool.True ->
1303           (match Pointers.eq_block ptr1.Pointers.pblock ptr2.Pointers.pblock with
1304            | Bool.True ->
1305              Types.Some
1306                (fE_of_bool
1307                  (Values.cmp_offset c ptr1.Pointers.poff ptr2.Pointers.poff))
1308            | Bool.False -> ev_cmp_mismatch c)
1309         | Bool.False -> Types.None))
1310
1311 (** val ev_cmpu :
1312     Integers.comparison -> Values.val0 -> Values.val0 -> Values.val0
1313     Types.option **)
1314 let ev_cmpu c v1 v2 =
1315   match v1 with
1316   | Values.Vundef -> Types.None
1317   | Values.Vint (sz1, n1) ->
1318     (match v2 with
1319      | Values.Vundef -> Types.None
1320      | Values.Vint (sz2, n2) ->
1321        AST.intsize_eq_elim sz1 sz2 n1 (fun n10 -> Types.Some
1322          (fE_of_bool (Values.cmpu_int (AST.bitsize_of_intsize sz2) c n10 n2)))
1323          Types.None
1324      | Values.Vnull -> Types.None
1325      | Values.Vptr x -> Types.None)
1326   | Values.Vnull -> Types.None
1327   | Values.Vptr x -> Types.None
1328
1329 (** val eval_binop :
1330     GenMem.mem -> AST.typ -> AST.typ -> AST.typ -> binary_operation ->
1331     Values.val0 -> Values.val0 -> Values.val0 Types.option **)
1332 let eval_binop m t1 t2 t' = function
1333 | Oadd (x, x0) -> ev_add
1334 | Osub (x, x0) -> ev_sub
1335 | Omul (x, x0) -> ev_mul
1336 | Odiv x -> ev_divs
1337 | Odivu x -> ev_divu
1338 | Omod x -> ev_mods
1339 | Omodu x -> ev_modu
1340 | Oand (x, x0) -> ev_and
1341 | Oor (x, x0) -> ev_or
1342 | Oxor (x, x0) -> ev_xor
1343 | Oshl (x, x0) -> ev_shl
1344 | Oshr (x, x0) -> ev_shr
1345 | Oshru (x, x0) -> ev_shru
1346 | Ocmp (x, x0, x1, c) -> ev_cmp c
1347 | Ocmpu (x, x0, c) -> ev_cmpu c
1348 | Oaddpi x -> ev_addpi
1349 | Oaddip x -> (fun x0 y -> ev_addpi y x0)
1350 | Osubpi x -> ev_subpi
1351 | Osubpp sz -> ev_subpp sz
1352 | Ocmpp (x, c) -> ev_cmpp m c
1353