extracted/csem.ml

   1 open Preamble
   2
   3 open Extra_bool
   4
   5 open Coqlib
   6
   7 open Values
   8
   9 open FrontEndVal
  10
  11 open Hide
  12
  13 open ByteValues
  14
  15 open Division
  16
  17 open Z
  18
  19 open BitVectorZ
  20
  21 open Pointers
  22
  23 open GenMem
  24
  25 open FrontEndMem
  26
  27 open Proper
  28
  29 open PositiveMap
  30
  31 open Deqsets
  32
  33 open Extralib
  34
  35 open Lists
  36
  37 open Identifiers
  38
  39 open Exp
  40
  41 open Arithmetic
  42
  43 open Vector
  44
  45 open Div_and_mod
  46
  47 open Util
  48
  49 open FoldStuff
  50
  51 open BitVector
  52
  53 open Extranat
  54
  55 open Integers
  56
  57 open AST
  58
  59 open ErrorMessages
  60
  61 open Option
  62
  63 open Setoids
  64
  65 open Monad
  66
  67 open Jmeq
  68
  69 open Russell
  70
  71 open Positive
  72
  73 open PreIdentifiers
  74
  75 open Bool
  76
  77 open Relations
  78
  79 open Nat
  80
  81 open List
  82
  83 open Hints_declaration
  84
  85 open Core_notation
  86
  87 open Pts
  88
  89 open Logic
  90
  91 open Types
  92
  93 open Errors
  94
  95 open Globalenvs
  96
  97 open CostLabel
  98
  99 open Csyntax
 100
 101 open Events
 102
 103 open Smallstep
 104
 105 open TypeComparison
 106
 107 open ClassifyOp
 108
 109 (** val sem_neg :
 110     Values.val0 -> Csyntax.type0 -> Values.val0 Types.option **)
 111 let rec sem_neg v = function
 112 | Csyntax.Tvoid -> Types.None
 113 | Csyntax.Tint (sz, x) ->
 114   (match v with
 115    | Values.Vundef -> Types.None
 116    | Values.Vint (sz', n) ->
 117      (match AST.eq_intsize sz sz' with
 118       | Bool.True ->
 119         Types.Some (Values.Vint (sz',
 120           (Arithmetic.two_complement_negation (AST.bitsize_of_intsize sz') n)))
 121       | Bool.False -> Types.None)
 122    | Values.Vnull -> Types.None
 123    | Values.Vptr x0 -> Types.None)
 124 | Csyntax.Tpointer x -> Types.None
 125 | Csyntax.Tarray (x, x0) -> Types.None
 126 | Csyntax.Tfunction (x, x0) -> Types.None
 127 | Csyntax.Tstruct (x, x0) -> Types.None
 128 | Csyntax.Tunion (x, x0) -> Types.None
 129 | Csyntax.Tcomp_ptr x -> Types.None
 130
 131 (** val sem_notint : Values.val0 -> Values.val0 Types.option **)
 132 let rec sem_notint = function
 133 | Values.Vundef -> Types.None
 134 | Values.Vint (sz, n) ->
 135   Types.Some (Values.Vint (sz,
 136     (BitVector.exclusive_disjunction_bv (AST.bitsize_of_intsize sz) n
 137       (Values.mone sz))))
 138 | Values.Vnull -> Types.None
 139 | Values.Vptr x -> Types.None
 140
 141 (** val sem_notbool :
 142     Values.val0 -> Csyntax.type0 -> Values.val0 Types.option **)
 143 let rec sem_notbool v = function
 144 | Csyntax.Tvoid -> Types.None
 145 | Csyntax.Tint (sz, x) ->
 146   (match v with
 147    | Values.Vundef -> Types.None
 148    | Values.Vint (sz', n) ->
 149      (match AST.eq_intsize sz sz' with
 150       | Bool.True ->
 151         Types.Some
 152           (Values.of_bool
 153             (BitVector.eq_bv (AST.bitsize_of_intsize sz') n
 154               (BitVector.zero (AST.bitsize_of_intsize sz'))))
 155       | Bool.False -> Types.None)
 156    | Values.Vnull -> Types.None
 157    | Values.Vptr x0 -> Types.None)
 158 | Csyntax.Tpointer x ->
 159   (match v with
 160    | Values.Vundef -> Types.None
 161    | Values.Vint (x0, x1) -> Types.None
 162    | Values.Vnull -> Types.Some Values.vtrue
 163    | Values.Vptr x0 -> Types.Some Values.vfalse)
 164 | Csyntax.Tarray (x, x0) -> Types.None
 165 | Csyntax.Tfunction (x, x0) -> Types.None
 166 | Csyntax.Tstruct (x, x0) -> Types.None
 167 | Csyntax.Tunion (x, x0) -> Types.None
 168 | Csyntax.Tcomp_ptr x -> Types.None
 169
 170 (** val sem_add :
 171     Values.val0 -> Csyntax.type0 -> Values.val0 -> Csyntax.type0 ->
 172     Values.val0 Types.option **)
 173 let rec sem_add v1 t1 v2 t2 =
 174   match ClassifyOp.classify_add t1 t2 with
 175   | ClassifyOp.Add_case_ii (x, x0) ->
 176     (match v1 with
 177      | Values.Vundef -> Types.None
 178      | Values.Vint (sz1, n1) ->
 179        (match v2 with
 180         | Values.Vundef -> Types.None
 181         | Values.Vint (sz2, n2) ->
 182           AST.intsize_eq_elim sz1 sz2 n1 (fun n10 -> Types.Some (Values.Vint
 183             (sz2,
 184             (Arithmetic.addition_n (AST.bitsize_of_intsize sz2) n10 n2))))
 185             Types.None
 186         | Values.Vnull -> Types.None
 187         | Values.Vptr x1 -> Types.None)
 188      | Values.Vnull -> Types.None
 189      | Values.Vptr x1 -> Types.None)
 190   | ClassifyOp.Add_case_pi (x, ty, x0, sg) ->
 191     (match v1 with
 192      | Values.Vundef -> Types.None
 193      | Values.Vint (x1, x2) -> Types.None
 194      | Values.Vnull ->
 195        (match v2 with
 196         | Values.Vundef -> Types.None
 197         | Values.Vint (sz2, n2) ->
 198           (match BitVector.eq_bv (AST.bitsize_of_intsize sz2) n2
 199                    (BitVector.zero (AST.bitsize_of_intsize sz2)) with
 200            | Bool.True -> Types.Some Values.Vnull
 201            | Bool.False -> Types.None)
 202         | Values.Vnull -> Types.None
 203         | Values.Vptr x1 -> Types.None)
 204      | Values.Vptr ptr1 ->
 205        (match v2 with
 206         | Values.Vundef -> Types.None
 207         | Values.Vint (sz2, n2) ->
 208           Types.Some (Values.Vptr
 209             (Pointers.shift_pointer_n (AST.bitsize_of_intsize sz2) ptr1
 210               (Csyntax.sizeof ty) sg n2))
 211         | Values.Vnull -> Types.None
 212         | Values.Vptr x1 -> Types.None))
 213   | ClassifyOp.Add_case_ip (x, x0, sg, ty) ->
 214     (match v1 with
 215      | Values.Vundef -> Types.None
 216      | Values.Vint (sz1, n1) ->
 217        (match v2 with
 218         | Values.Vundef -> Types.None
 219         | Values.Vint (x1, x2) -> Types.None
 220         | Values.Vnull ->
 221           (match BitVector.eq_bv (AST.bitsize_of_intsize sz1) n1
 222                    (BitVector.zero (AST.bitsize_of_intsize sz1)) with
 223            | Bool.True -> Types.Some Values.Vnull
 224            | Bool.False -> Types.None)
 225         | Values.Vptr ptr2 ->
 226           Types.Some (Values.Vptr
 227             (Pointers.shift_pointer_n (AST.bitsize_of_intsize sz1) ptr2
 228               (Csyntax.sizeof ty) sg n1)))
 229      | Values.Vnull -> Types.None
 230      | Values.Vptr x1 -> Types.None)
 231   | ClassifyOp.Add_default (x, x0) -> Types.None
 232
 233 (** val sem_sub :
 234     Values.val0 -> Csyntax.type0 -> Values.val0 -> Csyntax.type0 ->
 235     Csyntax.type0 -> Values.val0 Types.option **)
 236 let rec sem_sub v1 t1 v2 t2 target =
 237   match ClassifyOp.classify_sub t1 t2 with
 238   | ClassifyOp.Sub_case_ii (x, x0) ->
 239     (match v1 with
 240      | Values.Vundef -> Types.None
 241      | Values.Vint (sz1, n1) ->
 242        (match v2 with
 243         | Values.Vundef -> Types.None
 244         | Values.Vint (sz2, n2) ->
 245           AST.intsize_eq_elim sz1 sz2 n1 (fun n10 -> Types.Some (Values.Vint
 246             (sz2,
 247             (Arithmetic.subtraction (AST.bitsize_of_intsize sz2) n10 n2))))
 248             Types.None
 249         | Values.Vnull -> Types.None
 250         | Values.Vptr x1 -> Types.None)
 251      | Values.Vnull -> Types.None
 252      | Values.Vptr x1 -> Types.None)
 253   | ClassifyOp.Sub_case_pi (x, ty, x0, sg) ->
 254     (match v1 with
 255      | Values.Vundef -> Types.None
 256      | Values.Vint (x1, x2) -> Types.None
 257      | Values.Vnull ->
 258        (match v2 with
 259         | Values.Vundef -> Types.None
 260         | Values.Vint (sz2, n2) ->
 261           (match BitVector.eq_bv (AST.bitsize_of_intsize sz2) n2
 262                    (BitVector.zero (AST.bitsize_of_intsize sz2)) with
 263            | Bool.True -> Types.Some Values.Vnull
 264            | Bool.False -> Types.None)
 265         | Values.Vnull -> Types.None
 266         | Values.Vptr x1 -> Types.None)
 267      | Values.Vptr ptr1 ->
 268        (match v2 with
 269         | Values.Vundef -> Types.None
 270         | Values.Vint (sz2, n2) ->
 271           Types.Some (Values.Vptr
 272             (Pointers.neg_shift_pointer_n (AST.bitsize_of_intsize sz2) ptr1
 273               (Csyntax.sizeof ty) sg n2))
 274         | Values.Vnull -> Types.None
 275         | Values.Vptr x1 -> Types.None))
 276   | ClassifyOp.Sub_case_pp (x, x0, ty, x1) ->
 277     (match v1 with
 278      | Values.Vundef -> Types.None
 279      | Values.Vint (x2, x3) -> Types.None
 280      | Values.Vnull ->
 281        (match v2 with
 282         | Values.Vundef -> Types.None
 283         | Values.Vint (x2, x3) -> Types.None
 284         | Values.Vnull ->
 285           (match target with
 286            | Csyntax.Tvoid -> Types.None
 287            | Csyntax.Tint (tsz, tsg) ->
 288              Types.Some (Values.Vint (tsz,
 289                (BitVector.zero (AST.bitsize_of_intsize tsz))))
 290            | Csyntax.Tpointer x2 -> Types.None
 291            | Csyntax.Tarray (x2, x3) -> Types.None
 292            | Csyntax.Tfunction (x2, x3) -> Types.None
 293            | Csyntax.Tstruct (x2, x3) -> Types.None
 294            | Csyntax.Tunion (x2, x3) -> Types.None
 295            | Csyntax.Tcomp_ptr x2 -> Types.None)
 296         | Values.Vptr x2 -> Types.None)
 297      | Values.Vptr ptr1 ->
 298        (match v2 with
 299         | Values.Vundef -> Types.None
 300         | Values.Vint (x2, x3) -> Types.None
 301         | Values.Vnull -> Types.None
 302         | Values.Vptr ptr2 ->
 303           (match Pointers.eq_block ptr1.Pointers.pblock ptr2.Pointers.pblock with
 304            | Bool.True ->
 305              (match Nat.eqb (Csyntax.sizeof ty) Nat.O with
 306               | Bool.True -> Types.None
 307               | Bool.False ->
 308                 (match target with
 309                  | Csyntax.Tvoid -> Types.None
 310                  | Csyntax.Tint (tsz, tsg) ->
 311                    (match Arithmetic.division_u (Nat.S (Nat.S (Nat.S (Nat.S
 312                             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 313                             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 314                             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 315                             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 316                             Nat.O)))))))))))))))))))))))))))))))
 317                             (Pointers.sub_offset (Nat.S (Nat.S (Nat.S (Nat.S
 318                               (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 319                               (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 320                               (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 321                               (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 322                               (Nat.S (Nat.S (Nat.S (Nat.S
 323                               Nat.O))))))))))))))))))))))))))))))))
 324                               ptr1.Pointers.poff ptr2.Pointers.poff)
 325                             (Integers.repr (Csyntax.sizeof ty)) with
 326                     | Types.None -> Types.None
 327                     | Types.Some v ->
 328                       Types.Some (Values.Vint (tsz,
 329                         (Arithmetic.zero_ext (Nat.S (Nat.S (Nat.S (Nat.S
 330                           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 331                           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 332                           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 333                           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 334                           Nat.O))))))))))))))))))))))))))))))))
 335                           (AST.bitsize_of_intsize tsz) v))))
 336                  | Csyntax.Tpointer x2 -> Types.None
 337                  | Csyntax.Tarray (x2, x3) -> Types.None
 338                  | Csyntax.Tfunction (x2, x3) -> Types.None
 339                  | Csyntax.Tstruct (x2, x3) -> Types.None
 340                  | Csyntax.Tunion (x2, x3) -> Types.None
 341                  | Csyntax.Tcomp_ptr x2 -> Types.None))
 342            | Bool.False -> Types.None)))
 343   | ClassifyOp.Sub_default (x, x0) -> Types.None
 344
 345 (** val sem_mul :
 346     Values.val0 -> Csyntax.type0 -> Values.val0 -> Csyntax.type0 ->
 347     Values.val0 Types.option **)
 348 let rec sem_mul v1 t1 v2 t2 =
 349   match ClassifyOp.classify_aop t1 t2 with
 350   | ClassifyOp.Aop_case_ii (x, x0) ->
 351     (match v1 with
 352      | Values.Vundef -> Types.None
 353      | Values.Vint (sz1, n1) ->
 354        (match v2 with
 355         | Values.Vundef -> Types.None
 356         | Values.Vint (sz2, n2) ->
 357           AST.intsize_eq_elim sz1 sz2 n1 (fun n10 -> Types.Some (Values.Vint
 358             (sz2,
 359             (Arithmetic.short_multiplication (AST.bitsize_of_intsize sz2) n10
 360               n2)))) Types.None
 361         | Values.Vnull -> Types.None
 362         | Values.Vptr x1 -> Types.None)
 363      | Values.Vnull -> Types.None
 364      | Values.Vptr x1 -> Types.None)
 365   | ClassifyOp.Aop_default (x, x0) -> Types.None
 366
 367 (** val sem_div :
 368     Values.val0 -> Csyntax.type0 -> Values.val0 -> Csyntax.type0 ->
 369     Values.val0 Types.option **)
 370 let rec sem_div v1 t1 v2 t2 =
 371   match ClassifyOp.classify_aop t1 t2 with
 372   | ClassifyOp.Aop_case_ii (x, sg) ->
 373     (match v1 with
 374      | Values.Vundef -> Types.None
 375      | Values.Vint (sz1, n1) ->
 376        (match v2 with
 377         | Values.Vundef -> Types.None
 378         | Values.Vint (sz2, n2) ->
 379           (match sg with
 380            | AST.Signed ->
 381              AST.intsize_eq_elim sz1 sz2 n1 (fun n10 ->
 382                Types.option_map (fun x0 -> Values.Vint (sz2, x0))
 383                  (Arithmetic.division_s (AST.bitsize_of_intsize sz2) n10 n2))
 384                Types.None
 385            | AST.Unsigned ->
 386              AST.intsize_eq_elim sz1 sz2 n1 (fun n10 ->
 387                Types.option_map (fun x0 -> Values.Vint (sz2, x0))
 388                  (Arithmetic.division_u
 389                    (Nat.plus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 390                      Nat.O)))))))
 391                      (Nat.times (AST.pred_size_intsize sz2) (Nat.S (Nat.S
 392                        (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 393                        Nat.O)))))))))) n10 n2)) Types.None)
 394         | Values.Vnull -> Types.None
 395         | Values.Vptr x0 -> Types.None)
 396      | Values.Vnull -> Types.None
 397      | Values.Vptr x0 -> Types.None)
 398   | ClassifyOp.Aop_default (x, x0) -> Types.None
 399
 400 (** val sem_mod :
 401     Values.val0 -> Csyntax.type0 -> Values.val0 -> Csyntax.type0 ->
 402     Values.val0 Types.option **)
 403 let rec sem_mod v1 t1 v2 t2 =
 404   match ClassifyOp.classify_aop t1 t2 with
 405   | ClassifyOp.Aop_case_ii (sz, sg) ->
 406     (match v1 with
 407      | Values.Vundef -> Types.None
 408      | Values.Vint (sz1, n1) ->
 409        (match v2 with
 410         | Values.Vundef -> Types.None
 411         | Values.Vint (sz2, n2) ->
 412           (match sg with
 413            | AST.Signed ->
 414              AST.intsize_eq_elim sz1 sz2 n1 (fun n10 ->
 415                Types.option_map (fun x -> Values.Vint (sz2, x))
 416                  (Arithmetic.modulus_s (AST.bitsize_of_intsize sz2) n10 n2))
 417                Types.None
 418            | AST.Unsigned ->
 419              AST.intsize_eq_elim sz1 sz2 n1 (fun n10 ->
 420                Types.option_map (fun x -> Values.Vint (sz2, x))
 421                  (Arithmetic.modulus_u
 422                    (Nat.plus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 423                      Nat.O)))))))
 424                      (Nat.times (AST.pred_size_intsize sz2) (Nat.S (Nat.S
 425                        (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 426                        Nat.O)))))))))) n10 n2)) Types.None)
 427         | Values.Vnull -> Types.None
 428         | Values.Vptr x -> Types.None)
 429      | Values.Vnull -> Types.None
 430      | Values.Vptr x -> Types.None)
 431   | ClassifyOp.Aop_default (x, x0) -> Types.None
 432
 433 (** val sem_and : Values.val0 -> Values.val0 -> Values.val0 Types.option **)
 434 let rec sem_and v1 v2 =
 435   match v1 with
 436   | Values.Vundef -> Types.None
 437   | Values.Vint (sz1, n1) ->
 438     (match v2 with
 439      | Values.Vundef -> Types.None
 440      | Values.Vint (sz2, n2) ->
 441        AST.intsize_eq_elim sz1 sz2 n1 (fun n10 -> Types.Some (Values.Vint
 442          (sz2,
 443          (BitVector.conjunction_bv (AST.bitsize_of_intsize sz2) n10 n2))))
 444          Types.None
 445      | Values.Vnull -> Types.None
 446      | Values.Vptr x -> Types.None)
 447   | Values.Vnull -> Types.None
 448   | Values.Vptr x -> Types.None
 449
 450 (** val sem_or : Values.val0 -> Values.val0 -> Values.val0 Types.option **)
 451 let rec sem_or v1 v2 =
 452   match v1 with
 453   | Values.Vundef -> Types.None
 454   | Values.Vint (sz1, n1) ->
 455     (match v2 with
 456      | Values.Vundef -> Types.None
 457      | Values.Vint (sz2, n2) ->
 458        AST.intsize_eq_elim sz1 sz2 n1 (fun n10 -> Types.Some (Values.Vint
 459          (sz2,
 460          (BitVector.inclusive_disjunction_bv (AST.bitsize_of_intsize sz2) n10
 461            n2)))) Types.None
 462      | Values.Vnull -> Types.None
 463      | Values.Vptr x -> Types.None)
 464   | Values.Vnull -> Types.None
 465   | Values.Vptr x -> Types.None
 466
 467 (** val sem_xor : Values.val0 -> Values.val0 -> Values.val0 Types.option **)
 468 let rec sem_xor v1 v2 =
 469   match v1 with
 470   | Values.Vundef -> Types.None
 471   | Values.Vint (sz1, n1) ->
 472     (match v2 with
 473      | Values.Vundef -> Types.None
 474      | Values.Vint (sz2, n2) ->
 475        AST.intsize_eq_elim sz1 sz2 n1 (fun n10 -> Types.Some (Values.Vint
 476          (sz2,
 477          (BitVector.exclusive_disjunction_bv (AST.bitsize_of_intsize sz2) n10
 478            n2)))) Types.None
 479      | Values.Vnull -> Types.None
 480      | Values.Vptr x -> Types.None)
 481   | Values.Vnull -> Types.None
 482   | Values.Vptr x -> Types.None
 483
 484 (** val sem_shl : Values.val0 -> Values.val0 -> Values.val0 Types.option **)
 485 let rec sem_shl v1 v2 =
 486   match v1 with
 487   | Values.Vundef -> Types.None
 488   | Values.Vint (sz1, n1) ->
 489     (match v2 with
 490      | Values.Vundef -> Types.None
 491      | Values.Vint (sz2, n2) ->
 492        (match Arithmetic.lt_u (AST.bitsize_of_intsize sz2) n2
 493                 (Arithmetic.bitvector_of_nat (AST.bitsize_of_intsize sz2)
 494                   (AST.bitsize_of_intsize sz1)) with
 495         | Bool.True ->
 496           Types.Some (Values.Vint (sz1,
 497             (Vector.shift_left (AST.bitsize_of_intsize sz1)
 498               (Arithmetic.nat_of_bitvector (AST.bitsize_of_intsize sz2) n2)
 499               n1 Bool.False)))
 500         | Bool.False -> Types.None)
 501      | Values.Vnull -> Types.None
 502      | Values.Vptr x -> Types.None)
 503   | Values.Vnull -> Types.None
 504   | Values.Vptr x -> Types.None
 505
 506 (** val sem_shr :
 507     Values.val0 -> Csyntax.type0 -> Values.val0 -> Csyntax.type0 ->
 508     Values.val0 Types.option **)
 509 let rec sem_shr v1 t1 v2 t2 =
 510   match ClassifyOp.classify_aop t1 t2 with
 511   | ClassifyOp.Aop_case_ii (x, sg) ->
 512     (match v1 with
 513      | Values.Vundef -> Types.None
 514      | Values.Vint (sz1, n1) ->
 515        (match v2 with
 516         | Values.Vundef -> Types.None
 517         | Values.Vint (sz2, n2) ->
 518           (match sg with
 519            | AST.Signed ->
 520              (match Arithmetic.lt_u (AST.bitsize_of_intsize sz2) n2
 521                       (Arithmetic.bitvector_of_nat
 522                         (AST.bitsize_of_intsize sz2)
 523                         (AST.bitsize_of_intsize sz1)) with
 524               | Bool.True ->
 525                 Types.Some (Values.Vint (sz1,
 526                   (Vector.shift_right
 527                     (Nat.plus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 528                       (Nat.S Nat.O)))))))
 529                       (Nat.times (AST.pred_size_intsize sz1) (Nat.S (Nat.S
 530                         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 531                         Nat.O))))))))))
 532                     (Arithmetic.nat_of_bitvector (AST.bitsize_of_intsize sz2)
 533                       n2) n1
 534                     (Vector.head'
 535                       (Nat.plus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 536                         (Nat.S Nat.O)))))))
 537                         (Nat.times (AST.pred_size_intsize sz1) (Nat.S (Nat.S
 538                           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 539                           Nat.O)))))))))) n1))))
 540               | Bool.False -> Types.None)
 541            | AST.Unsigned ->
 542              (match Arithmetic.lt_u (AST.bitsize_of_intsize sz2) n2
 543                       (Arithmetic.bitvector_of_nat
 544                         (AST.bitsize_of_intsize sz2)
 545                         (AST.bitsize_of_intsize sz1)) with
 546               | Bool.True ->
 547                 Types.Some (Values.Vint (sz1,
 548                   (Vector.shift_right
 549                     (Nat.plus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 550                       (Nat.S Nat.O)))))))
 551                       (Nat.times (AST.pred_size_intsize sz1) (Nat.S (Nat.S
 552                         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 553                         Nat.O))))))))))
 554                     (Arithmetic.nat_of_bitvector (AST.bitsize_of_intsize sz2)
 555                       n2) n1 Bool.False)))
 556               | Bool.False -> Types.None))
 557         | Values.Vnull -> Types.None
 558         | Values.Vptr x0 -> Types.None)
 559      | Values.Vnull -> Types.None
 560      | Values.Vptr x0 -> Types.None)
 561   | ClassifyOp.Aop_default (x, x0) -> Types.None
 562
 563 (** val sem_cmp_mismatch :
 564     Integers.comparison -> Values.val0 Types.option **)
 565 let rec sem_cmp_mismatch = function
 566 | Integers.Ceq -> Types.Some Values.vfalse
 567 | Integers.Cne -> Types.Some Values.vtrue
 568 | Integers.Clt -> Types.None
 569 | Integers.Cle -> Types.None
 570 | Integers.Cgt -> Types.None
 571 | Integers.Cge -> Types.None
 572
 573 (** val sem_cmp_match : Integers.comparison -> Values.val0 Types.option **)
 574 let rec sem_cmp_match = function
 575 | Integers.Ceq -> Types.Some Values.vtrue
 576 | Integers.Cne -> Types.Some Values.vfalse
 577 | Integers.Clt -> Types.None
 578 | Integers.Cle -> Types.None
 579 | Integers.Cgt -> Types.None
 580 | Integers.Cge -> Types.None
 581
 582 (** val sem_cmp :
 583     Integers.comparison -> Values.val0 -> Csyntax.type0 -> Values.val0 ->
 584     Csyntax.type0 -> GenMem.mem -> Values.val0 Types.option **)
 585 let rec sem_cmp c v1 t1 v2 t2 m =
 586   match ClassifyOp.classify_cmp t1 t2 with
 587   | ClassifyOp.Cmp_case_ii (x, sg) ->
 588     (match v1 with
 589      | Values.Vundef -> Types.None
 590      | Values.Vint (sz1, n1) ->
 591        (match v2 with
 592         | Values.Vundef -> Types.None
 593         | Values.Vint (sz2, n2) ->
 594           (match sg with
 595            | AST.Signed ->
 596              AST.intsize_eq_elim sz1 sz2 n1 (fun n10 -> Types.Some
 597                (Values.of_bool
 598                  (Values.cmp_int (AST.bitsize_of_intsize sz2) c n10 n2)))
 599                Types.None
 600            | AST.Unsigned ->
 601              AST.intsize_eq_elim sz1 sz2 n1 (fun n10 -> Types.Some
 602                (Values.of_bool
 603                  (Values.cmpu_int (AST.bitsize_of_intsize sz2) c n10 n2)))
 604                Types.None)
 605         | Values.Vnull -> Types.None
 606         | Values.Vptr x0 -> Types.None)
 607      | Values.Vnull -> Types.None
 608      | Values.Vptr x0 -> Types.None)
 609   | ClassifyOp.Cmp_case_pp (x, x0) ->
 610     (match v1 with
 611      | Values.Vundef -> Types.None
 612      | Values.Vint (x1, x2) -> Types.None
 613      | Values.Vnull ->
 614        (match v2 with
 615         | Values.Vundef -> Types.None
 616         | Values.Vint (x1, x2) -> Types.None
 617         | Values.Vnull -> sem_cmp_match c
 618         | Values.Vptr ptr2 -> sem_cmp_mismatch c)
 619      | Values.Vptr ptr1 ->
 620        (match v2 with
 621         | Values.Vundef -> Types.None
 622         | Values.Vint (x1, x2) -> Types.None
 623         | Values.Vnull -> sem_cmp_mismatch c
 624         | Values.Vptr ptr2 ->
 625           (match Bool.andb (FrontEndMem.valid_pointer m ptr1)
 626                    (FrontEndMem.valid_pointer m ptr2) with
 627            | Bool.True ->
 628              (match Pointers.eq_block ptr1.Pointers.pblock
 629                       ptr2.Pointers.pblock with
 630               | Bool.True ->
 631                 Types.Some
 632                   (Values.of_bool
 633                     (Values.cmp_offset c ptr1.Pointers.poff
 634                       ptr2.Pointers.poff))
 635               | Bool.False -> sem_cmp_mismatch c)
 636            | Bool.False -> Types.None)))
 637   | ClassifyOp.Cmp_default (x, x0) -> Types.None
 638
 639 (** val cast_bool_to_target :
 640     Csyntax.type0 -> Values.val0 Types.option -> Values.val0 Types.option **)
 641 let cast_bool_to_target ty = function
 642 | Types.None -> Types.None
 643 | Types.Some v ->
 644   (match ty with
 645    | Csyntax.Tvoid -> Types.None
 646    | Csyntax.Tint (sz, sg) -> Types.Some (Values.zero_ext sz v)
 647    | Csyntax.Tpointer x -> Types.None
 648    | Csyntax.Tarray (x, x0) -> Types.None
 649    | Csyntax.Tfunction (x, x0) -> Types.None
 650    | Csyntax.Tstruct (x, x0) -> Types.None
 651    | Csyntax.Tunion (x, x0) -> Types.None
 652    | Csyntax.Tcomp_ptr x -> Types.None)
 653
 654 (** val sem_unary_operation :
 655     Csyntax.unary_operation -> Values.val0 -> Csyntax.type0 -> Values.val0
 656     Types.option **)
 657 let sem_unary_operation op v ty =
 658   match op with
 659   | Csyntax.Onotbool -> sem_notbool v ty
 660   | Csyntax.Onotint -> sem_notint v
 661   | Csyntax.Oneg -> sem_neg v ty
 662
 663 (** val sem_binary_operation :
 664     Csyntax.binary_operation -> Values.val0 -> Csyntax.type0 -> Values.val0
 665     -> Csyntax.type0 -> GenMem.mem -> Csyntax.type0 -> Values.val0
 666     Types.option **)
 667 let rec sem_binary_operation op v1 t1 v2 t2 m ty =
 668   match op with
 669   | Csyntax.Oadd -> sem_add v1 t1 v2 t2
 670   | Csyntax.Osub -> sem_sub v1 t1 v2 t2 ty
 671   | Csyntax.Omul -> sem_mul v1 t1 v2 t2
 672   | Csyntax.Odiv -> sem_div v1 t1 v2 t2
 673   | Csyntax.Omod -> sem_mod v1 t1 v2 t2
 674   | Csyntax.Oand -> sem_and v1 v2
 675   | Csyntax.Oor -> sem_or v1 v2
 676   | Csyntax.Oxor -> sem_xor v1 v2
 677   | Csyntax.Oshl -> sem_shl v1 v2
 678   | Csyntax.Oshr -> sem_shr v1 t1 v2 t2
 679   | Csyntax.Oeq ->
 680     cast_bool_to_target ty (sem_cmp Integers.Ceq v1 t1 v2 t2 m)
 681   | Csyntax.One ->
 682     cast_bool_to_target ty (sem_cmp Integers.Cne v1 t1 v2 t2 m)
 683   | Csyntax.Olt ->
 684     cast_bool_to_target ty (sem_cmp Integers.Clt v1 t1 v2 t2 m)
 685   | Csyntax.Ogt ->
 686     cast_bool_to_target ty (sem_cmp Integers.Cgt v1 t1 v2 t2 m)
 687   | Csyntax.Ole ->
 688     cast_bool_to_target ty (sem_cmp Integers.Cle v1 t1 v2 t2 m)
 689   | Csyntax.Oge ->
 690     cast_bool_to_target ty (sem_cmp Integers.Cge v1 t1 v2 t2 m)
 691
 692 (** val cast_int_int :
 693     AST.intsize -> AST.signedness -> AST.intsize -> BitVector.bitVector ->
 694     BitVector.bitVector **)
 695 let rec cast_int_int sz sg dstsz i =
 696   match sg with
 697   | AST.Signed ->
 698     Arithmetic.sign_ext (AST.bitsize_of_intsize sz)
 699       (AST.bitsize_of_intsize dstsz) i
 700   | AST.Unsigned ->
 701     Arithmetic.zero_ext (AST.bitsize_of_intsize sz)
 702       (AST.bitsize_of_intsize dstsz) i
 703
 704 type genv = Csyntax.clight_fundef Globalenvs.genv_t
 705
 706 type env = Pointers.block Identifiers.identifier_map
 707
 708 (** val empty_env : env **)
 709 let empty_env =
 710   Identifiers.empty_map PreIdentifiers.SymbolTag
 711
 712 (** val load_value_of_type :
 713     Csyntax.type0 -> GenMem.mem -> Pointers.block -> Pointers.offset ->
 714     Values.val0 Types.option **)
 715 let rec load_value_of_type ty m b ofs =
 716   match Csyntax.access_mode ty with
 717   | Csyntax.By_value chunk ->
 718     FrontEndMem.loadv chunk m (Values.Vptr { Pointers.pblock = b;
 719       Pointers.poff = ofs })
 720   | Csyntax.By_reference ->
 721     Types.Some (Values.Vptr { Pointers.pblock = b; Pointers.poff = ofs })
 722   | Csyntax.By_nothing x -> Types.None
 723
 724 (** val store_value_of_type :
 725     Csyntax.type0 -> GenMem.mem -> Pointers.block -> Pointers.offset ->
 726     Values.val0 -> GenMem.mem Types.option **)
 727 let rec store_value_of_type ty_dest m loc ofs v =
 728   match Csyntax.access_mode ty_dest with
 729   | Csyntax.By_value chunk ->
 730     FrontEndMem.storev chunk m (Values.Vptr { Pointers.pblock = loc;
 731       Pointers.poff = ofs }) v
 732   | Csyntax.By_reference -> Types.None
 733   | Csyntax.By_nothing x -> Types.None
 734
 735 (** val blocks_of_env : env -> Pointers.block List.list **)
 736 let blocks_of_env e =
 737   List.map (fun x -> x.Types.snd)
 738     (Identifiers.elements PreIdentifiers.SymbolTag e)
 739
 740 (** val select_switch :
 741     AST.intsize -> BitVector.bitVector -> Csyntax.labeled_statements ->
 742     Csyntax.labeled_statements Types.option **)
 743 let rec select_switch sz n sl = match sl with
 744 | Csyntax.LSdefault x -> Types.Some sl
 745 | Csyntax.LScase (sz', c, s, sl') ->
 746   AST.intsize_eq_elim sz sz' n (fun n0 ->
 747     match BitVector.eq_bv (AST.bitsize_of_intsize sz') c n0 with
 748     | Bool.True -> Types.Some sl
 749     | Bool.False -> select_switch sz' n0 sl') Types.None
 750
 751 (** val seq_of_labeled_statement :
 752     Csyntax.labeled_statements -> Csyntax.statement **)
 753 let rec seq_of_labeled_statement = function
 754 | Csyntax.LSdefault s -> s
 755 | Csyntax.LScase (x, c, s, sl') ->
 756   Csyntax.Ssequence (s, (seq_of_labeled_statement sl'))
 757
 758 type cont =
 759 | Kstop
 760 | Kseq of Csyntax.statement * cont
 761 | Kwhile of Csyntax.expr * Csyntax.statement * cont
 762 | Kdowhile of Csyntax.expr * Csyntax.statement * cont
 763 | Kfor2 of Csyntax.expr * Csyntax.statement * Csyntax.statement * cont
 764 | Kfor3 of Csyntax.expr * Csyntax.statement * Csyntax.statement * cont
 765 | Kswitch of cont
 766 | Kcall of ((Pointers.block, Pointers.offset) Types.prod, Csyntax.type0)
 767            Types.prod Types.option * Csyntax.function0 * env * cont
 768
 769 (** val cont_rect_Type4 :
 770     'a1 -> (Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
 771     Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
 772     Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
 773     Csyntax.statement -> Csyntax.statement -> cont -> 'a1 -> 'a1) ->
 774     (Csyntax.expr -> Csyntax.statement -> Csyntax.statement -> cont -> 'a1 ->
 775     'a1) -> (cont -> 'a1 -> 'a1) -> (((Pointers.block, Pointers.offset)
 776     Types.prod, Csyntax.type0) Types.prod Types.option -> Csyntax.function0
 777     -> env -> cont -> 'a1 -> 'a1) -> cont -> 'a1 **)
 778 let rec cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 h_Kswitch h_Kcall = function
 779 | Kstop -> h_Kstop
 780 | Kseq (x_8739, x_8738) ->
 781   h_Kseq x_8739 x_8738
 782     (cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
 783       h_Kswitch h_Kcall x_8738)
 784 | Kwhile (x_8742, x_8741, x_8740) ->
 785   h_Kwhile x_8742 x_8741 x_8740
 786     (cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
 787       h_Kswitch h_Kcall x_8740)
 788 | Kdowhile (x_8745, x_8744, x_8743) ->
 789   h_Kdowhile x_8745 x_8744 x_8743
 790     (cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
 791       h_Kswitch h_Kcall x_8743)
 792 | Kfor2 (x_8749, x_8748, x_8747, x_8746) ->
 793   h_Kfor2 x_8749 x_8748 x_8747 x_8746
 794     (cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
 795       h_Kswitch h_Kcall x_8746)
 796 | Kfor3 (x_8753, x_8752, x_8751, x_8750) ->
 797   h_Kfor3 x_8753 x_8752 x_8751 x_8750
 798     (cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
 799       h_Kswitch h_Kcall x_8750)
 800 | Kswitch x_8754 ->
 801   h_Kswitch x_8754
 802     (cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
 803       h_Kswitch h_Kcall x_8754)
 804 | Kcall (x_8758, x_8757, x_8756, x_8755) ->
 805   h_Kcall x_8758 x_8757 x_8756 x_8755
 806     (cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
 807       h_Kswitch h_Kcall x_8755)
 808
 809 (** val cont_rect_Type3 :
 810     'a1 -> (Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
 811     Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
 812     Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
 813     Csyntax.statement -> Csyntax.statement -> cont -> 'a1 -> 'a1) ->
 814     (Csyntax.expr -> Csyntax.statement -> Csyntax.statement -> cont -> 'a1 ->
 815     'a1) -> (cont -> 'a1 -> 'a1) -> (((Pointers.block, Pointers.offset)
 816     Types.prod, Csyntax.type0) Types.prod Types.option -> Csyntax.function0
 817     -> env -> cont -> 'a1 -> 'a1) -> cont -> 'a1 **)
 818 let rec cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 h_Kswitch h_Kcall = function
 819 | Kstop -> h_Kstop
 820 | Kseq (x_8799, x_8798) ->
 821   h_Kseq x_8799 x_8798
 822     (cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
 823       h_Kswitch h_Kcall x_8798)
 824 | Kwhile (x_8802, x_8801, x_8800) ->
 825   h_Kwhile x_8802 x_8801 x_8800
 826     (cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
 827       h_Kswitch h_Kcall x_8800)
 828 | Kdowhile (x_8805, x_8804, x_8803) ->
 829   h_Kdowhile x_8805 x_8804 x_8803
 830     (cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
 831       h_Kswitch h_Kcall x_8803)
 832 | Kfor2 (x_8809, x_8808, x_8807, x_8806) ->
 833   h_Kfor2 x_8809 x_8808 x_8807 x_8806
 834     (cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
 835       h_Kswitch h_Kcall x_8806)
 836 | Kfor3 (x_8813, x_8812, x_8811, x_8810) ->
 837   h_Kfor3 x_8813 x_8812 x_8811 x_8810
 838     (cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
 839       h_Kswitch h_Kcall x_8810)
 840 | Kswitch x_8814 ->
 841   h_Kswitch x_8814
 842     (cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
 843       h_Kswitch h_Kcall x_8814)
 844 | Kcall (x_8818, x_8817, x_8816, x_8815) ->
 845   h_Kcall x_8818 x_8817 x_8816 x_8815
 846     (cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
 847       h_Kswitch h_Kcall x_8815)
 848
 849 (** val cont_rect_Type2 :
 850     'a1 -> (Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
 851     Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
 852     Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
 853     Csyntax.statement -> Csyntax.statement -> cont -> 'a1 -> 'a1) ->
 854     (Csyntax.expr -> Csyntax.statement -> Csyntax.statement -> cont -> 'a1 ->
 855     'a1) -> (cont -> 'a1 -> 'a1) -> (((Pointers.block, Pointers.offset)
 856     Types.prod, Csyntax.type0) Types.prod Types.option -> Csyntax.function0
 857     -> env -> cont -> 'a1 -> 'a1) -> cont -> 'a1 **)
 858 let rec cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 h_Kswitch h_Kcall = function
 859 | Kstop -> h_Kstop
 860 | Kseq (x_8829, x_8828) ->
 861   h_Kseq x_8829 x_8828
 862     (cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
 863       h_Kswitch h_Kcall x_8828)
 864 | Kwhile (x_8832, x_8831, x_8830) ->
 865   h_Kwhile x_8832 x_8831 x_8830
 866     (cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
 867       h_Kswitch h_Kcall x_8830)
 868 | Kdowhile (x_8835, x_8834, x_8833) ->
 869   h_Kdowhile x_8835 x_8834 x_8833
 870     (cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
 871       h_Kswitch h_Kcall x_8833)
 872 | Kfor2 (x_8839, x_8838, x_8837, x_8836) ->
 873   h_Kfor2 x_8839 x_8838 x_8837 x_8836
 874     (cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
 875       h_Kswitch h_Kcall x_8836)
 876 | Kfor3 (x_8843, x_8842, x_8841, x_8840) ->
 877   h_Kfor3 x_8843 x_8842 x_8841 x_8840
 878     (cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
 879       h_Kswitch h_Kcall x_8840)
 880 | Kswitch x_8844 ->
 881   h_Kswitch x_8844
 882     (cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
 883       h_Kswitch h_Kcall x_8844)
 884 | Kcall (x_8848, x_8847, x_8846, x_8845) ->
 885   h_Kcall x_8848 x_8847 x_8846 x_8845
 886     (cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
 887       h_Kswitch h_Kcall x_8845)
 888
 889 (** val cont_rect_Type1 :
 890     'a1 -> (Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
 891     Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
 892     Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
 893     Csyntax.statement -> Csyntax.statement -> cont -> 'a1 -> 'a1) ->
 894     (Csyntax.expr -> Csyntax.statement -> Csyntax.statement -> cont -> 'a1 ->
 895     'a1) -> (cont -> 'a1 -> 'a1) -> (((Pointers.block, Pointers.offset)
 896     Types.prod, Csyntax.type0) Types.prod Types.option -> Csyntax.function0
 897     -> env -> cont -> 'a1 -> 'a1) -> cont -> 'a1 **)
 898 let rec cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 h_Kswitch h_Kcall = function
 899 | Kstop -> h_Kstop
 900 | Kseq (x_8859, x_8858) ->
 901   h_Kseq x_8859 x_8858
 902     (cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
 903       h_Kswitch h_Kcall x_8858)
 904 | Kwhile (x_8862, x_8861, x_8860) ->
 905   h_Kwhile x_8862 x_8861 x_8860
 906     (cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
 907       h_Kswitch h_Kcall x_8860)
 908 | Kdowhile (x_8865, x_8864, x_8863) ->
 909   h_Kdowhile x_8865 x_8864 x_8863
 910     (cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
 911       h_Kswitch h_Kcall x_8863)
 912 | Kfor2 (x_8869, x_8868, x_8867, x_8866) ->
 913   h_Kfor2 x_8869 x_8868 x_8867 x_8866
 914     (cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
 915       h_Kswitch h_Kcall x_8866)
 916 | Kfor3 (x_8873, x_8872, x_8871, x_8870) ->
 917   h_Kfor3 x_8873 x_8872 x_8871 x_8870
 918     (cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
 919       h_Kswitch h_Kcall x_8870)
 920 | Kswitch x_8874 ->
 921   h_Kswitch x_8874
 922     (cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
 923       h_Kswitch h_Kcall x_8874)
 924 | Kcall (x_8878, x_8877, x_8876, x_8875) ->
 925   h_Kcall x_8878 x_8877 x_8876 x_8875
 926     (cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
 927       h_Kswitch h_Kcall x_8875)
 928
 929 (** val cont_rect_Type0 :
 930     'a1 -> (Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
 931     Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
 932     Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
 933     Csyntax.statement -> Csyntax.statement -> cont -> 'a1 -> 'a1) ->
 934     (Csyntax.expr -> Csyntax.statement -> Csyntax.statement -> cont -> 'a1 ->
 935     'a1) -> (cont -> 'a1 -> 'a1) -> (((Pointers.block, Pointers.offset)
 936     Types.prod, Csyntax.type0) Types.prod Types.option -> Csyntax.function0
 937     -> env -> cont -> 'a1 -> 'a1) -> cont -> 'a1 **)
 938 let rec cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 h_Kswitch h_Kcall = function
 939 | Kstop -> h_Kstop
 940 | Kseq (x_8889, x_8888) ->
 941   h_Kseq x_8889 x_8888
 942     (cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
 943       h_Kswitch h_Kcall x_8888)
 944 | Kwhile (x_8892, x_8891, x_8890) ->
 945   h_Kwhile x_8892 x_8891 x_8890
 946     (cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
 947       h_Kswitch h_Kcall x_8890)
 948 | Kdowhile (x_8895, x_8894, x_8893) ->
 949   h_Kdowhile x_8895 x_8894 x_8893
 950     (cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
 951       h_Kswitch h_Kcall x_8893)
 952 | Kfor2 (x_8899, x_8898, x_8897, x_8896) ->
 953   h_Kfor2 x_8899 x_8898 x_8897 x_8896
 954     (cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
 955       h_Kswitch h_Kcall x_8896)
 956 | Kfor3 (x_8903, x_8902, x_8901, x_8900) ->
 957   h_Kfor3 x_8903 x_8902 x_8901 x_8900
 958     (cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
 959       h_Kswitch h_Kcall x_8900)
 960 | Kswitch x_8904 ->
 961   h_Kswitch x_8904
 962     (cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
 963       h_Kswitch h_Kcall x_8904)
 964 | Kcall (x_8908, x_8907, x_8906, x_8905) ->
 965   h_Kcall x_8908 x_8907 x_8906 x_8905
 966     (cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
 967       h_Kswitch h_Kcall x_8905)
 968
 969 (** val cont_inv_rect_Type4 :
 970     cont -> (__ -> 'a1) -> (Csyntax.statement -> cont -> (__ -> 'a1) -> __ ->
 971     'a1) -> (Csyntax.expr -> Csyntax.statement -> cont -> (__ -> 'a1) -> __
 972     -> 'a1) -> (Csyntax.expr -> Csyntax.statement -> cont -> (__ -> 'a1) ->
 973     __ -> 'a1) -> (Csyntax.expr -> Csyntax.statement -> Csyntax.statement ->
 974     cont -> (__ -> 'a1) -> __ -> 'a1) -> (Csyntax.expr -> Csyntax.statement
 975     -> Csyntax.statement -> cont -> (__ -> 'a1) -> __ -> 'a1) -> (cont -> (__
 976     -> 'a1) -> __ -> 'a1) -> (((Pointers.block, Pointers.offset) Types.prod,
 977     Csyntax.type0) Types.prod Types.option -> Csyntax.function0 -> env ->
 978     cont -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 **)
 979 let cont_inv_rect_Type4 hterm h1 h2 h3 h4 h5 h6 h7 h8 =
 980   let hcut = cont_rect_Type4 h1 h2 h3 h4 h5 h6 h7 h8 hterm in hcut __
 981
 982 (** val cont_inv_rect_Type3 :
 983     cont -> (__ -> 'a1) -> (Csyntax.statement -> cont -> (__ -> 'a1) -> __ ->
 984     'a1) -> (Csyntax.expr -> Csyntax.statement -> cont -> (__ -> 'a1) -> __
 985     -> 'a1) -> (Csyntax.expr -> Csyntax.statement -> cont -> (__ -> 'a1) ->
 986     __ -> 'a1) -> (Csyntax.expr -> Csyntax.statement -> Csyntax.statement ->
 987     cont -> (__ -> 'a1) -> __ -> 'a1) -> (Csyntax.expr -> Csyntax.statement
 988     -> Csyntax.statement -> cont -> (__ -> 'a1) -> __ -> 'a1) -> (cont -> (__
 989     -> 'a1) -> __ -> 'a1) -> (((Pointers.block, Pointers.offset) Types.prod,
 990     Csyntax.type0) Types.prod Types.option -> Csyntax.function0 -> env ->
 991     cont -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 **)
 992 let cont_inv_rect_Type3 hterm h1 h2 h3 h4 h5 h6 h7 h8 =
 993   let hcut = cont_rect_Type3 h1 h2 h3 h4 h5 h6 h7 h8 hterm in hcut __
 994
 995 (** val cont_inv_rect_Type2 :
 996     cont -> (__ -> 'a1) -> (Csyntax.statement -> cont -> (__ -> 'a1) -> __ ->
 997     'a1) -> (Csyntax.expr -> Csyntax.statement -> cont -> (__ -> 'a1) -> __
 998     -> 'a1) -> (Csyntax.expr -> Csyntax.statement -> cont -> (__ -> 'a1) ->
 999     __ -> 'a1) -> (Csyntax.expr -> Csyntax.statement -> Csyntax.statement ->
1000     cont -> (__ -> 'a1) -> __ -> 'a1) -> (Csyntax.expr -> Csyntax.statement
1001     -> Csyntax.statement -> cont -> (__ -> 'a1) -> __ -> 'a1) -> (cont -> (__
1002     -> 'a1) -> __ -> 'a1) -> (((Pointers.block, Pointers.offset) Types.prod,
1003     Csyntax.type0) Types.prod Types.option -> Csyntax.function0 -> env ->
1004     cont -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 **)
1005 let cont_inv_rect_Type2 hterm h1 h2 h3 h4 h5 h6 h7 h8 =
1006   let hcut = cont_rect_Type2 h1 h2 h3 h4 h5 h6 h7 h8 hterm in hcut __
1007
1008 (** val cont_inv_rect_Type1 :
1009     cont -> (__ -> 'a1) -> (Csyntax.statement -> cont -> (__ -> 'a1) -> __ ->
1010     'a1) -> (Csyntax.expr -> Csyntax.statement -> cont -> (__ -> 'a1) -> __
1011     -> 'a1) -> (Csyntax.expr -> Csyntax.statement -> cont -> (__ -> 'a1) ->
1012     __ -> 'a1) -> (Csyntax.expr -> Csyntax.statement -> Csyntax.statement ->
1013     cont -> (__ -> 'a1) -> __ -> 'a1) -> (Csyntax.expr -> Csyntax.statement
1014     -> Csyntax.statement -> cont -> (__ -> 'a1) -> __ -> 'a1) -> (cont -> (__
1015     -> 'a1) -> __ -> 'a1) -> (((Pointers.block, Pointers.offset) Types.prod,
1016     Csyntax.type0) Types.prod Types.option -> Csyntax.function0 -> env ->
1017     cont -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 **)
1018 let cont_inv_rect_Type1 hterm h1 h2 h3 h4 h5 h6 h7 h8 =
1019   let hcut = cont_rect_Type1 h1 h2 h3 h4 h5 h6 h7 h8 hterm in hcut __
1020
1021 (** val cont_inv_rect_Type0 :
1022     cont -> (__ -> 'a1) -> (Csyntax.statement -> cont -> (__ -> 'a1) -> __ ->
1023     'a1) -> (Csyntax.expr -> Csyntax.statement -> cont -> (__ -> 'a1) -> __
1024     -> 'a1) -> (Csyntax.expr -> Csyntax.statement -> cont -> (__ -> 'a1) ->
1025     __ -> 'a1) -> (Csyntax.expr -> Csyntax.statement -> Csyntax.statement ->
1026     cont -> (__ -> 'a1) -> __ -> 'a1) -> (Csyntax.expr -> Csyntax.statement
1027     -> Csyntax.statement -> cont -> (__ -> 'a1) -> __ -> 'a1) -> (cont -> (__
1028     -> 'a1) -> __ -> 'a1) -> (((Pointers.block, Pointers.offset) Types.prod,
1029     Csyntax.type0) Types.prod Types.option -> Csyntax.function0 -> env ->
1030     cont -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 **)
1031 let cont_inv_rect_Type0 hterm h1 h2 h3 h4 h5 h6 h7 h8 =
1032   let hcut = cont_rect_Type0 h1 h2 h3 h4 h5 h6 h7 h8 hterm in hcut __
1033
1034 (** val cont_discr : cont -> cont -> __ **)
1035 let cont_discr x y =
1036   Logic.eq_rect_Type2 x
1037     (match x with
1038      | Kstop -> Obj.magic (fun _ dH -> dH)
1039      | Kseq (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
1040      | Kwhile (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
1041      | Kdowhile (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
1042      | Kfor2 (a0, a1, a2, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
1043      | Kfor3 (a0, a1, a2, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
1044      | Kswitch a0 -> Obj.magic (fun _ dH -> dH __)
1045      | Kcall (a0, a1, a2, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)) y
1046
1047 (** val cont_jmdiscr : cont -> cont -> __ **)
1048 let cont_jmdiscr x y =
1049   Logic.eq_rect_Type2 x
1050     (match x with
1051      | Kstop -> Obj.magic (fun _ dH -> dH)
1052      | Kseq (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
1053      | Kwhile (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
1054      | Kdowhile (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
1055      | Kfor2 (a0, a1, a2, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
1056      | Kfor3 (a0, a1, a2, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
1057      | Kswitch a0 -> Obj.magic (fun _ dH -> dH __)
1058      | Kcall (a0, a1, a2, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)) y
1059
1060 (** val call_cont : cont -> cont **)
1061 let rec call_cont k = match k with
1062 | Kstop -> k
1063 | Kseq (s, k0) -> call_cont k0
1064 | Kwhile (e, s, k0) -> call_cont k0
1065 | Kdowhile (e, s, k0) -> call_cont k0
1066 | Kfor2 (e2, e3, s, k0) -> call_cont k0
1067 | Kfor3 (e2, e3, s, k0) -> call_cont k0
1068 | Kswitch k0 -> call_cont k0
1069 | Kcall (x, x0, x1, x2) -> k
1070
1071 type state =
1072 | State of Csyntax.function0 * Csyntax.statement * cont * env * GenMem.mem
1073 | Callstate of AST.ident * Csyntax.clight_fundef * Values.val0 List.list
1074    * cont * GenMem.mem
1075 | Returnstate of Values.val0 * cont * GenMem.mem
1076 | Finalstate of Integers.int
1077
1078 (** val state_rect_Type4 :
1079     (Csyntax.function0 -> Csyntax.statement -> cont -> env -> GenMem.mem ->
1080     'a1) -> (AST.ident -> Csyntax.clight_fundef -> Values.val0 List.list ->
1081     cont -> GenMem.mem -> 'a1) -> (Values.val0 -> cont -> GenMem.mem -> 'a1)
1082     -> (Integers.int -> 'a1) -> state -> 'a1 **)
1083 let rec state_rect_Type4 h_State h_Callstate h_Returnstate h_Finalstate = function
1084 | State (f, s, k, e, m) -> h_State f s k e m
1085 | Callstate (id, fd, args, k, m) -> h_Callstate id fd args k m
1086 | Returnstate (res, k, m) -> h_Returnstate res k m
1087 | Finalstate r -> h_Finalstate r
1088
1089 (** val state_rect_Type5 :
1090     (Csyntax.function0 -> Csyntax.statement -> cont -> env -> GenMem.mem ->
1091     'a1) -> (AST.ident -> Csyntax.clight_fundef -> Values.val0 List.list ->
1092     cont -> GenMem.mem -> 'a1) -> (Values.val0 -> cont -> GenMem.mem -> 'a1)
1093     -> (Integers.int -> 'a1) -> state -> 'a1 **)
1094 let rec state_rect_Type5 h_State h_Callstate h_Returnstate h_Finalstate = function
1095 | State (f, s, k, e, m) -> h_State f s k e m
1096 | Callstate (id, fd, args, k, m) -> h_Callstate id fd args k m
1097 | Returnstate (res, k, m) -> h_Returnstate res k m
1098 | Finalstate r -> h_Finalstate r
1099
1100 (** val state_rect_Type3 :
1101     (Csyntax.function0 -> Csyntax.statement -> cont -> env -> GenMem.mem ->
1102     'a1) -> (AST.ident -> Csyntax.clight_fundef -> Values.val0 List.list ->
1103     cont -> GenMem.mem -> 'a1) -> (Values.val0 -> cont -> GenMem.mem -> 'a1)
1104     -> (Integers.int -> 'a1) -> state -> 'a1 **)
1105 let rec state_rect_Type3 h_State h_Callstate h_Returnstate h_Finalstate = function
1106 | State (f, s, k, e, m) -> h_State f s k e m
1107 | Callstate (id, fd, args, k, m) -> h_Callstate id fd args k m
1108 | Returnstate (res, k, m) -> h_Returnstate res k m
1109 | Finalstate r -> h_Finalstate r
1110
1111 (** val state_rect_Type2 :
1112     (Csyntax.function0 -> Csyntax.statement -> cont -> env -> GenMem.mem ->
1113     'a1) -> (AST.ident -> Csyntax.clight_fundef -> Values.val0 List.list ->
1114     cont -> GenMem.mem -> 'a1) -> (Values.val0 -> cont -> GenMem.mem -> 'a1)
1115     -> (Integers.int -> 'a1) -> state -> 'a1 **)
1116 let rec state_rect_Type2 h_State h_Callstate h_Returnstate h_Finalstate = function
1117 | State (f, s, k, e, m) -> h_State f s k e m
1118 | Callstate (id, fd, args, k, m) -> h_Callstate id fd args k m
1119 | Returnstate (res, k, m) -> h_Returnstate res k m
1120 | Finalstate r -> h_Finalstate r
1121
1122 (** val state_rect_Type1 :
1123     (Csyntax.function0 -> Csyntax.statement -> cont -> env -> GenMem.mem ->
1124     'a1) -> (AST.ident -> Csyntax.clight_fundef -> Values.val0 List.list ->
1125     cont -> GenMem.mem -> 'a1) -> (Values.val0 -> cont -> GenMem.mem -> 'a1)
1126     -> (Integers.int -> 'a1) -> state -> 'a1 **)
1127 let rec state_rect_Type1 h_State h_Callstate h_Returnstate h_Finalstate = function
1128 | State (f, s, k, e, m) -> h_State f s k e m
1129 | Callstate (id, fd, args, k, m) -> h_Callstate id fd args k m
1130 | Returnstate (res, k, m) -> h_Returnstate res k m
1131 | Finalstate r -> h_Finalstate r
1132
1133 (** val state_rect_Type0 :
1134     (Csyntax.function0 -> Csyntax.statement -> cont -> env -> GenMem.mem ->
1135     'a1) -> (AST.ident -> Csyntax.clight_fundef -> Values.val0 List.list ->
1136     cont -> GenMem.mem -> 'a1) -> (Values.val0 -> cont -> GenMem.mem -> 'a1)
1137     -> (Integers.int -> 'a1) -> state -> 'a1 **)
1138 let rec state_rect_Type0 h_State h_Callstate h_Returnstate h_Finalstate = function
1139 | State (f, s, k, e, m) -> h_State f s k e m
1140 | Callstate (id, fd, args, k, m) -> h_Callstate id fd args k m
1141 | Returnstate (res, k, m) -> h_Returnstate res k m
1142 | Finalstate r -> h_Finalstate r
1143
1144 (** val state_inv_rect_Type4 :
1145     state -> (Csyntax.function0 -> Csyntax.statement -> cont -> env ->
1146     GenMem.mem -> __ -> 'a1) -> (AST.ident -> Csyntax.clight_fundef ->
1147     Values.val0 List.list -> cont -> GenMem.mem -> __ -> 'a1) -> (Values.val0
1148     -> cont -> GenMem.mem -> __ -> 'a1) -> (Integers.int -> __ -> 'a1) -> 'a1 **)
1149 let state_inv_rect_Type4 hterm h1 h2 h3 h4 =
1150   let hcut = state_rect_Type4 h1 h2 h3 h4 hterm in hcut __
1151
1152 (** val state_inv_rect_Type3 :
1153     state -> (Csyntax.function0 -> Csyntax.statement -> cont -> env ->
1154     GenMem.mem -> __ -> 'a1) -> (AST.ident -> Csyntax.clight_fundef ->
1155     Values.val0 List.list -> cont -> GenMem.mem -> __ -> 'a1) -> (Values.val0
1156     -> cont -> GenMem.mem -> __ -> 'a1) -> (Integers.int -> __ -> 'a1) -> 'a1 **)
1157 let state_inv_rect_Type3 hterm h1 h2 h3 h4 =
1158   let hcut = state_rect_Type3 h1 h2 h3 h4 hterm in hcut __
1159
1160 (** val state_inv_rect_Type2 :
1161     state -> (Csyntax.function0 -> Csyntax.statement -> cont -> env ->
1162     GenMem.mem -> __ -> 'a1) -> (AST.ident -> Csyntax.clight_fundef ->
1163     Values.val0 List.list -> cont -> GenMem.mem -> __ -> 'a1) -> (Values.val0
1164     -> cont -> GenMem.mem -> __ -> 'a1) -> (Integers.int -> __ -> 'a1) -> 'a1 **)
1165 let state_inv_rect_Type2 hterm h1 h2 h3 h4 =
1166   let hcut = state_rect_Type2 h1 h2 h3 h4 hterm in hcut __
1167
1168 (** val state_inv_rect_Type1 :
1169     state -> (Csyntax.function0 -> Csyntax.statement -> cont -> env ->
1170     GenMem.mem -> __ -> 'a1) -> (AST.ident -> Csyntax.clight_fundef ->
1171     Values.val0 List.list -> cont -> GenMem.mem -> __ -> 'a1) -> (Values.val0
1172     -> cont -> GenMem.mem -> __ -> 'a1) -> (Integers.int -> __ -> 'a1) -> 'a1 **)
1173 let state_inv_rect_Type1 hterm h1 h2 h3 h4 =
1174   let hcut = state_rect_Type1 h1 h2 h3 h4 hterm in hcut __
1175
1176 (** val state_inv_rect_Type0 :
1177     state -> (Csyntax.function0 -> Csyntax.statement -> cont -> env ->
1178     GenMem.mem -> __ -> 'a1) -> (AST.ident -> Csyntax.clight_fundef ->
1179     Values.val0 List.list -> cont -> GenMem.mem -> __ -> 'a1) -> (Values.val0
1180     -> cont -> GenMem.mem -> __ -> 'a1) -> (Integers.int -> __ -> 'a1) -> 'a1 **)
1181 let state_inv_rect_Type0 hterm h1 h2 h3 h4 =
1182   let hcut = state_rect_Type0 h1 h2 h3 h4 hterm in hcut __
1183
1184 (** val state_discr : state -> state -> __ **)
1185 let state_discr x y =
1186   Logic.eq_rect_Type2 x
1187     (match x with
1188      | State (a0, a1, a2, a3, a4) ->
1189        Obj.magic (fun _ dH -> dH __ __ __ __ __)
1190      | Callstate (a0, a1, a2, a3, a4) ->
1191        Obj.magic (fun _ dH -> dH __ __ __ __ __)
1192      | Returnstate (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
1193      | Finalstate a0 -> Obj.magic (fun _ dH -> dH __)) y
1194
1195 (** val state_jmdiscr : state -> state -> __ **)
1196 let state_jmdiscr x y =
1197   Logic.eq_rect_Type2 x
1198     (match x with
1199      | State (a0, a1, a2, a3, a4) ->
1200        Obj.magic (fun _ dH -> dH __ __ __ __ __)
1201      | Callstate (a0, a1, a2, a3, a4) ->
1202        Obj.magic (fun _ dH -> dH __ __ __ __ __)
1203      | Returnstate (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
1204      | Finalstate a0 -> Obj.magic (fun _ dH -> dH __)) y
1205
1206 (** val find_label :
1207     Csyntax.label -> Csyntax.statement -> cont -> (Csyntax.statement, cont)
1208     Types.prod Types.option **)
1209 let rec find_label lbl s k =
1210   match s with
1211   | Csyntax.Sskip -> Types.None
1212   | Csyntax.Sassign (x, x0) -> Types.None
1213   | Csyntax.Scall (x, x0, x1) -> Types.None
1214   | Csyntax.Ssequence (s1, s2) ->
1215     (match find_label lbl s1 (Kseq (s2, k)) with
1216      | Types.None -> find_label lbl s2 k
1217      | Types.Some sk -> Types.Some sk)
1218   | Csyntax.Sifthenelse (a, s1, s2) ->
1219     (match find_label lbl s1 k with
1220      | Types.None -> find_label lbl s2 k
1221      | Types.Some sk -> Types.Some sk)
1222   | Csyntax.Swhile (a, s1) -> find_label lbl s1 (Kwhile (a, s1, k))
1223   | Csyntax.Sdowhile (a, s1) -> find_label lbl s1 (Kdowhile (a, s1, k))
1224   | Csyntax.Sfor (a1, a2, a3, s1) ->
1225     (match find_label lbl a1 (Kseq ((Csyntax.Sfor (Csyntax.Sskip, a2, a3,
1226              s1)), k)) with
1227      | Types.None ->
1228        (match find_label lbl s1 (Kfor2 (a2, a3, s1, k)) with
1229         | Types.None -> find_label lbl a3 (Kfor3 (a2, a3, s1, k))
1230         | Types.Some sk -> Types.Some sk)
1231      | Types.Some sk -> Types.Some sk)
1232   | Csyntax.Sbreak -> Types.None
1233   | Csyntax.Scontinue -> Types.None
1234   | Csyntax.Sreturn x -> Types.None
1235   | Csyntax.Sswitch (e, sl) -> find_label_ls lbl sl (Kswitch k)
1236   | Csyntax.Slabel (lbl', s') ->
1237     (match AST.ident_eq lbl lbl' with
1238      | Types.Inl _ -> Types.Some { Types.fst = s'; Types.snd = k }
1239      | Types.Inr _ -> find_label lbl s' k)
1240   | Csyntax.Sgoto x -> Types.None
1241   | Csyntax.Scost (c, s') -> find_label lbl s' k
1242 (** val find_label_ls :
1243     Csyntax.label -> Csyntax.labeled_statements -> cont ->
1244     (Csyntax.statement, cont) Types.prod Types.option **)
1245 and find_label_ls lbl sl k =
1246   match sl with
1247   | Csyntax.LSdefault s -> find_label lbl s k
1248   | Csyntax.LScase (x, x0, s, sl') ->
1249     (match find_label lbl s (Kseq ((seq_of_labeled_statement sl'), k)) with
1250      | Types.None -> find_label_ls lbl sl' k
1251      | Types.Some sk -> Types.Some sk)
1252
1253 (** val fun_typeof : Csyntax.expr -> Csyntax.type0 **)
1254 let fun_typeof e =
1255   match Csyntax.typeof e with
1256   | Csyntax.Tvoid -> Csyntax.Tvoid
1257   | Csyntax.Tint (a, b) -> Csyntax.Tint (a, b)
1258   | Csyntax.Tpointer ty -> ty
1259   | Csyntax.Tarray (a, b) -> Csyntax.Tarray (a, b)
1260   | Csyntax.Tfunction (a, b) -> Csyntax.Tfunction (a, b)
1261   | Csyntax.Tstruct (a, b) -> Csyntax.Tstruct (a, b)
1262   | Csyntax.Tunion (a, b) -> Csyntax.Tunion (a, b)
1263   | Csyntax.Tcomp_ptr a -> Csyntax.Tcomp_ptr a
1264