open Preamble

open Extra_bool

open Coqlib

open Values

open FrontEndVal

open Hide

open ByteValues

open Division

open Z

open BitVectorZ

open Pointers

open GenMem

open FrontEndMem

open Proper

open PositiveMap

open Deqsets

open Extralib

open Lists

open Identifiers

open Exp

open Arithmetic

open Vector

open Div_and_mod

open Util

open FoldStuff

open BitVector

open Extranat

open Integers

open AST

open ErrorMessages

open Option

open Setoids

open Monad

open Jmeq

open Russell

open Positive

open PreIdentifiers

open Bool

open Relations

open Nat

open List

open Hints_declaration

open Core_notation

open Pts

open Logic

open Types

open Errors

open Globalenvs

open CostLabel

open Csyntax

open Events

open Smallstep

open TypeComparison

open ClassifyOp

(** val sem_neg :
    Values.val0 -> Csyntax.type0 -> Values.val0 Types.option **)
let rec sem_neg v = function
| Csyntax.Tvoid -> Types.None
| Csyntax.Tint (sz, x) ->
  (match v with
   | Values.Vundef -> Types.None
   | Values.Vint (sz', n) ->
     (match AST.eq_intsize sz sz' with
      | Bool.True ->
        Types.Some (Values.Vint (sz',
          (Arithmetic.two_complement_negation (AST.bitsize_of_intsize sz') n)))
      | Bool.False -> Types.None)
   | Values.Vnull -> Types.None
   | Values.Vptr x0 -> Types.None)
| Csyntax.Tpointer x -> Types.None
| Csyntax.Tarray (x, x0) -> Types.None
| Csyntax.Tfunction (x, x0) -> Types.None
| Csyntax.Tstruct (x, x0) -> Types.None
| Csyntax.Tunion (x, x0) -> Types.None
| Csyntax.Tcomp_ptr x -> Types.None

(** val sem_notint : Values.val0 -> Values.val0 Types.option **)
let rec sem_notint = function
| Values.Vundef -> Types.None
| Values.Vint (sz, n) ->
  Types.Some (Values.Vint (sz,
    (BitVector.exclusive_disjunction_bv (AST.bitsize_of_intsize sz) n
      (Values.mone sz))))
| Values.Vnull -> Types.None
| Values.Vptr x -> Types.None

(** val sem_notbool :
    Values.val0 -> Csyntax.type0 -> Values.val0 Types.option **)
let rec sem_notbool v = function
| Csyntax.Tvoid -> Types.None
| Csyntax.Tint (sz, x) ->
  (match v with
   | Values.Vundef -> Types.None
   | Values.Vint (sz', n) ->
     (match AST.eq_intsize sz sz' with
      | Bool.True ->
        Types.Some
          (Values.of_bool
            (BitVector.eq_bv (AST.bitsize_of_intsize sz') n
              (BitVector.zero (AST.bitsize_of_intsize sz'))))
      | Bool.False -> Types.None)
   | Values.Vnull -> Types.None
   | Values.Vptr x0 -> Types.None)
| Csyntax.Tpointer x ->
  (match v with
   | Values.Vundef -> Types.None
   | Values.Vint (x0, x1) -> Types.None
   | Values.Vnull -> Types.Some Values.vtrue
   | Values.Vptr x0 -> Types.Some Values.vfalse)
| Csyntax.Tarray (x, x0) -> Types.None
| Csyntax.Tfunction (x, x0) -> Types.None
| Csyntax.Tstruct (x, x0) -> Types.None
| Csyntax.Tunion (x, x0) -> Types.None
| Csyntax.Tcomp_ptr x -> Types.None

(** val sem_add :
    Values.val0 -> Csyntax.type0 -> Values.val0 -> Csyntax.type0 ->
    Values.val0 Types.option **)
let rec sem_add v1 t1 v2 t2 =
  match ClassifyOp.classify_add t1 t2 with
  | ClassifyOp.Add_case_ii (x, x0) ->
    (match v1 with
     | Values.Vundef -> Types.None
     | Values.Vint (sz1, n1) ->
       (match v2 with
        | Values.Vundef -> Types.None
        | Values.Vint (sz2, n2) ->
          AST.intsize_eq_elim sz1 sz2 n1 (fun n10 -> Types.Some (Values.Vint
            (sz2,
            (Arithmetic.addition_n (AST.bitsize_of_intsize sz2) n10 n2))))
            Types.None
        | Values.Vnull -> Types.None
        | Values.Vptr x1 -> Types.None)
     | Values.Vnull -> Types.None
     | Values.Vptr x1 -> Types.None)
  | ClassifyOp.Add_case_pi (x, ty, x0, sg) ->
    (match v1 with
     | Values.Vundef -> Types.None
     | Values.Vint (x1, x2) -> Types.None
     | Values.Vnull ->
       (match v2 with
        | Values.Vundef -> Types.None
        | Values.Vint (sz2, n2) ->
          (match BitVector.eq_bv (AST.bitsize_of_intsize sz2) n2
                   (BitVector.zero (AST.bitsize_of_intsize sz2)) with
           | Bool.True -> Types.Some Values.Vnull
           | Bool.False -> Types.None)
        | Values.Vnull -> Types.None
        | Values.Vptr x1 -> Types.None)
     | Values.Vptr ptr1 ->
       (match v2 with
        | Values.Vundef -> Types.None
        | Values.Vint (sz2, n2) ->
          Types.Some (Values.Vptr
            (Pointers.shift_pointer_n (AST.bitsize_of_intsize sz2) ptr1
              (Csyntax.sizeof ty) sg n2))
        | Values.Vnull -> Types.None
        | Values.Vptr x1 -> Types.None))
  | ClassifyOp.Add_case_ip (x, x0, sg, ty) ->
    (match v1 with
     | Values.Vundef -> Types.None
     | Values.Vint (sz1, n1) ->
       (match v2 with
        | Values.Vundef -> Types.None
        | Values.Vint (x1, x2) -> Types.None
        | Values.Vnull ->
          (match BitVector.eq_bv (AST.bitsize_of_intsize sz1) n1
                   (BitVector.zero (AST.bitsize_of_intsize sz1)) with
           | Bool.True -> Types.Some Values.Vnull
           | Bool.False -> Types.None)
        | Values.Vptr ptr2 ->
          Types.Some (Values.Vptr
            (Pointers.shift_pointer_n (AST.bitsize_of_intsize sz1) ptr2
              (Csyntax.sizeof ty) sg n1)))
     | Values.Vnull -> Types.None
     | Values.Vptr x1 -> Types.None)
  | ClassifyOp.Add_default (x, x0) -> Types.None

(** val sem_sub :
    Values.val0 -> Csyntax.type0 -> Values.val0 -> Csyntax.type0 ->
    Csyntax.type0 -> Values.val0 Types.option **)
let rec sem_sub v1 t1 v2 t2 target =
  match ClassifyOp.classify_sub t1 t2 with
  | ClassifyOp.Sub_case_ii (x, x0) ->
    (match v1 with
     | Values.Vundef -> Types.None
     | Values.Vint (sz1, n1) ->
       (match v2 with
        | Values.Vundef -> Types.None
        | Values.Vint (sz2, n2) ->
          AST.intsize_eq_elim sz1 sz2 n1 (fun n10 -> Types.Some (Values.Vint
            (sz2,
            (Arithmetic.subtraction (AST.bitsize_of_intsize sz2) n10 n2))))
            Types.None
        | Values.Vnull -> Types.None
        | Values.Vptr x1 -> Types.None)
     | Values.Vnull -> Types.None
     | Values.Vptr x1 -> Types.None)
  | ClassifyOp.Sub_case_pi (x, ty, x0, sg) ->
    (match v1 with
     | Values.Vundef -> Types.None
     | Values.Vint (x1, x2) -> Types.None
     | Values.Vnull ->
       (match v2 with
        | Values.Vundef -> Types.None
        | Values.Vint (sz2, n2) ->
          (match BitVector.eq_bv (AST.bitsize_of_intsize sz2) n2
                   (BitVector.zero (AST.bitsize_of_intsize sz2)) with
           | Bool.True -> Types.Some Values.Vnull
           | Bool.False -> Types.None)
        | Values.Vnull -> Types.None
        | Values.Vptr x1 -> Types.None)
     | Values.Vptr ptr1 ->
       (match v2 with
        | Values.Vundef -> Types.None
        | Values.Vint (sz2, n2) ->
          Types.Some (Values.Vptr
            (Pointers.neg_shift_pointer_n (AST.bitsize_of_intsize sz2) ptr1
              (Csyntax.sizeof ty) sg n2))
        | Values.Vnull -> Types.None
        | Values.Vptr x1 -> Types.None))
  | ClassifyOp.Sub_case_pp (x, x0, ty, x1) ->
    (match v1 with
     | Values.Vundef -> Types.None
     | Values.Vint (x2, x3) -> Types.None
     | Values.Vnull ->
       (match v2 with
        | Values.Vundef -> Types.None
        | Values.Vint (x2, x3) -> Types.None
        | Values.Vnull ->
          (match target with
           | Csyntax.Tvoid -> Types.None
           | Csyntax.Tint (tsz, tsg) ->
             Types.Some (Values.Vint (tsz,
               (BitVector.zero (AST.bitsize_of_intsize tsz))))
           | Csyntax.Tpointer x2 -> Types.None
           | Csyntax.Tarray (x2, x3) -> Types.None
           | Csyntax.Tfunction (x2, x3) -> Types.None
           | Csyntax.Tstruct (x2, x3) -> Types.None
           | Csyntax.Tunion (x2, x3) -> Types.None
           | Csyntax.Tcomp_ptr x2 -> Types.None)
        | Values.Vptr x2 -> Types.None)
     | Values.Vptr ptr1 ->
       (match v2 with
        | Values.Vundef -> Types.None
        | Values.Vint (x2, x3) -> Types.None
        | Values.Vnull -> Types.None
        | Values.Vptr ptr2 ->
          (match Pointers.eq_block ptr1.Pointers.pblock ptr2.Pointers.pblock with
           | Bool.True ->
             (match Nat.eqb (Csyntax.sizeof ty) Nat.O with
              | Bool.True -> Types.None
              | Bool.False ->
                (match target with
                 | Csyntax.Tvoid -> Types.None
                 | Csyntax.Tint (tsz, tsg) ->
                   (match Arithmetic.division_u (Nat.S (Nat.S (Nat.S (Nat.S
                            (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                            (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                            (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                            (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                            Nat.O)))))))))))))))))))))))))))))))
                            (Pointers.sub_offset (Nat.S (Nat.S (Nat.S (Nat.S
                              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                              (Nat.S (Nat.S (Nat.S (Nat.S
                              Nat.O))))))))))))))))))))))))))))))))
                              ptr1.Pointers.poff ptr2.Pointers.poff)
                            (Integers.repr (Csyntax.sizeof ty)) with
                    | Types.None -> Types.None
                    | Types.Some v ->
                      Types.Some (Values.Vint (tsz,
                        (Arithmetic.zero_ext (Nat.S (Nat.S (Nat.S (Nat.S
                          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                          Nat.O))))))))))))))))))))))))))))))))
                          (AST.bitsize_of_intsize tsz) v))))
                 | Csyntax.Tpointer x2 -> Types.None
                 | Csyntax.Tarray (x2, x3) -> Types.None
                 | Csyntax.Tfunction (x2, x3) -> Types.None
                 | Csyntax.Tstruct (x2, x3) -> Types.None
                 | Csyntax.Tunion (x2, x3) -> Types.None
                 | Csyntax.Tcomp_ptr x2 -> Types.None))
           | Bool.False -> Types.None)))
  | ClassifyOp.Sub_default (x, x0) -> Types.None

(** val sem_mul :
    Values.val0 -> Csyntax.type0 -> Values.val0 -> Csyntax.type0 ->
    Values.val0 Types.option **)
let rec sem_mul v1 t1 v2 t2 =
  match ClassifyOp.classify_aop t1 t2 with
  | ClassifyOp.Aop_case_ii (x, x0) ->
    (match v1 with
     | Values.Vundef -> Types.None
     | Values.Vint (sz1, n1) ->
       (match v2 with
        | Values.Vundef -> Types.None
        | Values.Vint (sz2, n2) ->
          AST.intsize_eq_elim sz1 sz2 n1 (fun n10 -> Types.Some (Values.Vint
            (sz2,
            (Arithmetic.short_multiplication (AST.bitsize_of_intsize sz2) n10
              n2)))) Types.None
        | Values.Vnull -> Types.None
        | Values.Vptr x1 -> Types.None)
     | Values.Vnull -> Types.None
     | Values.Vptr x1 -> Types.None)
  | ClassifyOp.Aop_default (x, x0) -> Types.None

(** val sem_div :
    Values.val0 -> Csyntax.type0 -> Values.val0 -> Csyntax.type0 ->
    Values.val0 Types.option **)
let rec sem_div v1 t1 v2 t2 =
  match ClassifyOp.classify_aop t1 t2 with
  | ClassifyOp.Aop_case_ii (x, sg) ->
    (match v1 with
     | Values.Vundef -> Types.None
     | Values.Vint (sz1, n1) ->
       (match v2 with
        | Values.Vundef -> Types.None
        | Values.Vint (sz2, n2) ->
          (match sg with
           | AST.Signed ->
             AST.intsize_eq_elim sz1 sz2 n1 (fun n10 ->
               Types.option_map (fun x0 -> Values.Vint (sz2, x0))
                 (Arithmetic.division_s (AST.bitsize_of_intsize sz2) n10 n2))
               Types.None
           | AST.Unsigned ->
             AST.intsize_eq_elim sz1 sz2 n1 (fun n10 ->
               Types.option_map (fun x0 -> Values.Vint (sz2, x0))
                 (Arithmetic.division_u
                   (Nat.plus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                     Nat.O)))))))
                     (Nat.times (AST.pred_size_intsize sz2) (Nat.S (Nat.S
                       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                       Nat.O)))))))))) n10 n2)) Types.None)
        | Values.Vnull -> Types.None
        | Values.Vptr x0 -> Types.None)
     | Values.Vnull -> Types.None
     | Values.Vptr x0 -> Types.None)
  | ClassifyOp.Aop_default (x, x0) -> Types.None

(** val sem_mod :
    Values.val0 -> Csyntax.type0 -> Values.val0 -> Csyntax.type0 ->
    Values.val0 Types.option **)
let rec sem_mod v1 t1 v2 t2 =
  match ClassifyOp.classify_aop t1 t2 with
  | ClassifyOp.Aop_case_ii (sz, sg) ->
    (match v1 with
     | Values.Vundef -> Types.None
     | Values.Vint (sz1, n1) ->
       (match v2 with
        | Values.Vundef -> Types.None
        | Values.Vint (sz2, n2) ->
          (match sg with
           | AST.Signed ->
             AST.intsize_eq_elim sz1 sz2 n1 (fun n10 ->
               Types.option_map (fun x -> Values.Vint (sz2, x))
                 (Arithmetic.modulus_s (AST.bitsize_of_intsize sz2) n10 n2))
               Types.None
           | AST.Unsigned ->
             AST.intsize_eq_elim sz1 sz2 n1 (fun n10 ->
               Types.option_map (fun x -> Values.Vint (sz2, x))
                 (Arithmetic.modulus_u
                   (Nat.plus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                     Nat.O)))))))
                     (Nat.times (AST.pred_size_intsize sz2) (Nat.S (Nat.S
                       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                       Nat.O)))))))))) n10 n2)) Types.None)
        | Values.Vnull -> Types.None
        | Values.Vptr x -> Types.None)
     | Values.Vnull -> Types.None
     | Values.Vptr x -> Types.None)
  | ClassifyOp.Aop_default (x, x0) -> Types.None

(** val sem_and : Values.val0 -> Values.val0 -> Values.val0 Types.option **)
let rec sem_and v1 v2 =
  match v1 with
  | Values.Vundef -> Types.None
  | Values.Vint (sz1, n1) ->
    (match v2 with
     | Values.Vundef -> Types.None
     | Values.Vint (sz2, n2) ->
       AST.intsize_eq_elim sz1 sz2 n1 (fun n10 -> Types.Some (Values.Vint
         (sz2,
         (BitVector.conjunction_bv (AST.bitsize_of_intsize sz2) n10 n2))))
         Types.None
     | Values.Vnull -> Types.None
     | Values.Vptr x -> Types.None)
  | Values.Vnull -> Types.None
  | Values.Vptr x -> Types.None

(** val sem_or : Values.val0 -> Values.val0 -> Values.val0 Types.option **)
let rec sem_or v1 v2 =
  match v1 with
  | Values.Vundef -> Types.None
  | Values.Vint (sz1, n1) ->
    (match v2 with
     | Values.Vundef -> Types.None
     | Values.Vint (sz2, n2) ->
       AST.intsize_eq_elim sz1 sz2 n1 (fun n10 -> Types.Some (Values.Vint
         (sz2,
         (BitVector.inclusive_disjunction_bv (AST.bitsize_of_intsize sz2) n10
           n2)))) Types.None
     | Values.Vnull -> Types.None
     | Values.Vptr x -> Types.None)
  | Values.Vnull -> Types.None
  | Values.Vptr x -> Types.None

(** val sem_xor : Values.val0 -> Values.val0 -> Values.val0 Types.option **)
let rec sem_xor v1 v2 =
  match v1 with
  | Values.Vundef -> Types.None
  | Values.Vint (sz1, n1) ->
    (match v2 with
     | Values.Vundef -> Types.None
     | Values.Vint (sz2, n2) ->
       AST.intsize_eq_elim sz1 sz2 n1 (fun n10 -> Types.Some (Values.Vint
         (sz2,
         (BitVector.exclusive_disjunction_bv (AST.bitsize_of_intsize sz2) n10
           n2)))) Types.None
     | Values.Vnull -> Types.None
     | Values.Vptr x -> Types.None)
  | Values.Vnull -> Types.None
  | Values.Vptr x -> Types.None

(** val sem_shl : Values.val0 -> Values.val0 -> Values.val0 Types.option **)
let rec sem_shl v1 v2 =
  match v1 with
  | Values.Vundef -> Types.None
  | Values.Vint (sz1, n1) ->
    (match v2 with
     | Values.Vundef -> Types.None
     | Values.Vint (sz2, n2) ->
       (match Arithmetic.lt_u (AST.bitsize_of_intsize sz2) n2
                (Arithmetic.bitvector_of_nat (AST.bitsize_of_intsize sz2)
                  (AST.bitsize_of_intsize sz1)) with
        | Bool.True ->
          Types.Some (Values.Vint (sz1,
            (Vector.shift_left (AST.bitsize_of_intsize sz1)
              (Arithmetic.nat_of_bitvector (AST.bitsize_of_intsize sz2) n2)
              n1 Bool.False)))
        | Bool.False -> Types.None)
     | Values.Vnull -> Types.None
     | Values.Vptr x -> Types.None)
  | Values.Vnull -> Types.None
  | Values.Vptr x -> Types.None

(** val sem_shr :
    Values.val0 -> Csyntax.type0 -> Values.val0 -> Csyntax.type0 ->
    Values.val0 Types.option **)
let rec sem_shr v1 t1 v2 t2 =
  match ClassifyOp.classify_aop t1 t2 with
  | ClassifyOp.Aop_case_ii (x, sg) ->
    (match v1 with
     | Values.Vundef -> Types.None
     | Values.Vint (sz1, n1) ->
       (match v2 with
        | Values.Vundef -> Types.None
        | Values.Vint (sz2, n2) ->
          (match sg with
           | AST.Signed ->
             (match Arithmetic.lt_u (AST.bitsize_of_intsize sz2) n2
                      (Arithmetic.bitvector_of_nat
                        (AST.bitsize_of_intsize sz2)
                        (AST.bitsize_of_intsize sz1)) with
              | Bool.True ->
                Types.Some (Values.Vint (sz1,
                  (Vector.shift_right
                    (Nat.plus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                      (Nat.S Nat.O)))))))
                      (Nat.times (AST.pred_size_intsize sz1) (Nat.S (Nat.S
                        (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                        Nat.O))))))))))
                    (Arithmetic.nat_of_bitvector (AST.bitsize_of_intsize sz2)
                      n2) n1
                    (Vector.head'
                      (Nat.plus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                        (Nat.S Nat.O)))))))
                        (Nat.times (AST.pred_size_intsize sz1) (Nat.S (Nat.S
                          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                          Nat.O)))))))))) n1))))
              | Bool.False -> Types.None)
           | AST.Unsigned ->
             (match Arithmetic.lt_u (AST.bitsize_of_intsize sz2) n2
                      (Arithmetic.bitvector_of_nat
                        (AST.bitsize_of_intsize sz2)
                        (AST.bitsize_of_intsize sz1)) with
              | Bool.True ->
                Types.Some (Values.Vint (sz1,
                  (Vector.shift_right
                    (Nat.plus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                      (Nat.S Nat.O)))))))
                      (Nat.times (AST.pred_size_intsize sz1) (Nat.S (Nat.S
                        (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                        Nat.O))))))))))
                    (Arithmetic.nat_of_bitvector (AST.bitsize_of_intsize sz2)
                      n2) n1 Bool.False)))
              | Bool.False -> Types.None))
        | Values.Vnull -> Types.None
        | Values.Vptr x0 -> Types.None)
     | Values.Vnull -> Types.None
     | Values.Vptr x0 -> Types.None)
  | ClassifyOp.Aop_default (x, x0) -> Types.None

(** val sem_cmp_mismatch :
    Integers.comparison -> Values.val0 Types.option **)
let rec sem_cmp_mismatch = function
| Integers.Ceq -> Types.Some Values.vfalse
| Integers.Cne -> Types.Some Values.vtrue
| Integers.Clt -> Types.None
| Integers.Cle -> Types.None
| Integers.Cgt -> Types.None
| Integers.Cge -> Types.None

(** val sem_cmp_match : Integers.comparison -> Values.val0 Types.option **)
let rec sem_cmp_match = function
| Integers.Ceq -> Types.Some Values.vtrue
| Integers.Cne -> Types.Some Values.vfalse
| Integers.Clt -> Types.None
| Integers.Cle -> Types.None
| Integers.Cgt -> Types.None
| Integers.Cge -> Types.None

(** val sem_cmp :
    Integers.comparison -> Values.val0 -> Csyntax.type0 -> Values.val0 ->
    Csyntax.type0 -> GenMem.mem -> Values.val0 Types.option **)
let rec sem_cmp c v1 t1 v2 t2 m =
  match ClassifyOp.classify_cmp t1 t2 with
  | ClassifyOp.Cmp_case_ii (x, sg) ->
    (match v1 with
     | Values.Vundef -> Types.None
     | Values.Vint (sz1, n1) ->
       (match v2 with
        | Values.Vundef -> Types.None
        | Values.Vint (sz2, n2) ->
          (match sg with
           | AST.Signed ->
             AST.intsize_eq_elim sz1 sz2 n1 (fun n10 -> Types.Some
               (Values.of_bool
                 (Values.cmp_int (AST.bitsize_of_intsize sz2) c n10 n2)))
               Types.None
           | AST.Unsigned ->
             AST.intsize_eq_elim sz1 sz2 n1 (fun n10 -> Types.Some
               (Values.of_bool
                 (Values.cmpu_int (AST.bitsize_of_intsize sz2) c n10 n2)))
               Types.None)
        | Values.Vnull -> Types.None
        | Values.Vptr x0 -> Types.None)
     | Values.Vnull -> Types.None
     | Values.Vptr x0 -> Types.None)
  | ClassifyOp.Cmp_case_pp (x, x0) ->
    (match v1 with
     | Values.Vundef -> Types.None
     | Values.Vint (x1, x2) -> Types.None
     | Values.Vnull ->
       (match v2 with
        | Values.Vundef -> Types.None
        | Values.Vint (x1, x2) -> Types.None
        | Values.Vnull -> sem_cmp_match c
        | Values.Vptr ptr2 -> sem_cmp_mismatch c)
     | Values.Vptr ptr1 ->
       (match v2 with
        | Values.Vundef -> Types.None
        | Values.Vint (x1, x2) -> Types.None
        | Values.Vnull -> sem_cmp_mismatch c
        | Values.Vptr ptr2 ->
          (match Bool.andb (FrontEndMem.valid_pointer m ptr1)
                   (FrontEndMem.valid_pointer m ptr2) with
           | Bool.True ->
             (match Pointers.eq_block ptr1.Pointers.pblock
                      ptr2.Pointers.pblock with
              | Bool.True ->
                Types.Some
                  (Values.of_bool
                    (Values.cmp_offset c ptr1.Pointers.poff
                      ptr2.Pointers.poff))
              | Bool.False -> sem_cmp_mismatch c)
           | Bool.False -> Types.None)))
  | ClassifyOp.Cmp_default (x, x0) -> Types.None

(** val cast_bool_to_target :
    Csyntax.type0 -> Values.val0 Types.option -> Values.val0 Types.option **)
let cast_bool_to_target ty = function
| Types.None -> Types.None
| Types.Some v ->
  (match ty with
   | Csyntax.Tvoid -> Types.None
   | Csyntax.Tint (sz, sg) -> Types.Some (Values.zero_ext sz v)
   | Csyntax.Tpointer x -> Types.None
   | Csyntax.Tarray (x, x0) -> Types.None
   | Csyntax.Tfunction (x, x0) -> Types.None
   | Csyntax.Tstruct (x, x0) -> Types.None
   | Csyntax.Tunion (x, x0) -> Types.None
   | Csyntax.Tcomp_ptr x -> Types.None)

(** val sem_unary_operation :
    Csyntax.unary_operation -> Values.val0 -> Csyntax.type0 -> Values.val0
    Types.option **)
let sem_unary_operation op v ty =
  match op with
  | Csyntax.Onotbool -> sem_notbool v ty
  | Csyntax.Onotint -> sem_notint v
  | Csyntax.Oneg -> sem_neg v ty

(** val sem_binary_operation :
    Csyntax.binary_operation -> Values.val0 -> Csyntax.type0 -> Values.val0
    -> Csyntax.type0 -> GenMem.mem -> Csyntax.type0 -> Values.val0
    Types.option **)
let rec sem_binary_operation op v1 t1 v2 t2 m ty =
  match op with
  | Csyntax.Oadd -> sem_add v1 t1 v2 t2
  | Csyntax.Osub -> sem_sub v1 t1 v2 t2 ty
  | Csyntax.Omul -> sem_mul v1 t1 v2 t2
  | Csyntax.Odiv -> sem_div v1 t1 v2 t2
  | Csyntax.Omod -> sem_mod v1 t1 v2 t2
  | Csyntax.Oand -> sem_and v1 v2
  | Csyntax.Oor -> sem_or v1 v2
  | Csyntax.Oxor -> sem_xor v1 v2
  | Csyntax.Oshl -> sem_shl v1 v2
  | Csyntax.Oshr -> sem_shr v1 t1 v2 t2
  | Csyntax.Oeq ->
    cast_bool_to_target ty (sem_cmp Integers.Ceq v1 t1 v2 t2 m)
  | Csyntax.One ->
    cast_bool_to_target ty (sem_cmp Integers.Cne v1 t1 v2 t2 m)
  | Csyntax.Olt ->
    cast_bool_to_target ty (sem_cmp Integers.Clt v1 t1 v2 t2 m)
  | Csyntax.Ogt ->
    cast_bool_to_target ty (sem_cmp Integers.Cgt v1 t1 v2 t2 m)
  | Csyntax.Ole ->
    cast_bool_to_target ty (sem_cmp Integers.Cle v1 t1 v2 t2 m)
  | Csyntax.Oge ->
    cast_bool_to_target ty (sem_cmp Integers.Cge v1 t1 v2 t2 m)

(** val cast_int_int :
    AST.intsize -> AST.signedness -> AST.intsize -> BitVector.bitVector ->
    BitVector.bitVector **)
let rec cast_int_int sz sg dstsz i =
  match sg with
  | AST.Signed ->
    Arithmetic.sign_ext (AST.bitsize_of_intsize sz)
      (AST.bitsize_of_intsize dstsz) i
  | AST.Unsigned ->
    Arithmetic.zero_ext (AST.bitsize_of_intsize sz)
      (AST.bitsize_of_intsize dstsz) i

type genv = Csyntax.clight_fundef Globalenvs.genv_t

type env = Pointers.block Identifiers.identifier_map

(** val empty_env : env **)
let empty_env =
  Identifiers.empty_map PreIdentifiers.SymbolTag

(** val load_value_of_type :
    Csyntax.type0 -> GenMem.mem -> Pointers.block -> Pointers.offset ->
    Values.val0 Types.option **)
let rec load_value_of_type ty m b ofs =
  match Csyntax.access_mode ty with
  | Csyntax.By_value chunk ->
    FrontEndMem.loadv chunk m (Values.Vptr { Pointers.pblock = b;
      Pointers.poff = ofs })
  | Csyntax.By_reference ->
    Types.Some (Values.Vptr { Pointers.pblock = b; Pointers.poff = ofs })
  | Csyntax.By_nothing x -> Types.None

(** val store_value_of_type :
    Csyntax.type0 -> GenMem.mem -> Pointers.block -> Pointers.offset ->
    Values.val0 -> GenMem.mem Types.option **)
let rec store_value_of_type ty_dest m loc ofs v =
  match Csyntax.access_mode ty_dest with
  | Csyntax.By_value chunk ->
    FrontEndMem.storev chunk m (Values.Vptr { Pointers.pblock = loc;
      Pointers.poff = ofs }) v
  | Csyntax.By_reference -> Types.None
  | Csyntax.By_nothing x -> Types.None

(** val blocks_of_env : env -> Pointers.block List.list **)
let blocks_of_env e =
  List.map (fun x -> x.Types.snd)
    (Identifiers.elements PreIdentifiers.SymbolTag e)

(** val select_switch :
    AST.intsize -> BitVector.bitVector -> Csyntax.labeled_statements ->
    Csyntax.labeled_statements Types.option **)
let rec select_switch sz n sl = match sl with
| Csyntax.LSdefault x -> Types.Some sl
| Csyntax.LScase (sz', c, s, sl') ->
  AST.intsize_eq_elim sz sz' n (fun n0 ->
    match BitVector.eq_bv (AST.bitsize_of_intsize sz') c n0 with
    | Bool.True -> Types.Some sl
    | Bool.False -> select_switch sz' n0 sl') Types.None

(** val seq_of_labeled_statement :
    Csyntax.labeled_statements -> Csyntax.statement **)
let rec seq_of_labeled_statement = function
| Csyntax.LSdefault s -> s
| Csyntax.LScase (x, c, s, sl') ->
  Csyntax.Ssequence (s, (seq_of_labeled_statement sl'))

type cont =
| Kstop
| Kseq of Csyntax.statement * cont
| Kwhile of Csyntax.expr * Csyntax.statement * cont
| Kdowhile of Csyntax.expr * Csyntax.statement * cont
| Kfor2 of Csyntax.expr * Csyntax.statement * Csyntax.statement * cont
| Kfor3 of Csyntax.expr * Csyntax.statement * Csyntax.statement * cont
| Kswitch of cont
| Kcall of ((Pointers.block, Pointers.offset) Types.prod, Csyntax.type0)
           Types.prod Types.option * Csyntax.function0 * env * cont

(** val cont_rect_Type4 :
    'a1 -> (Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
    Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
    Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
    Csyntax.statement -> Csyntax.statement -> cont -> 'a1 -> 'a1) ->
    (Csyntax.expr -> Csyntax.statement -> Csyntax.statement -> cont -> 'a1 ->
    'a1) -> (cont -> 'a1 -> 'a1) -> (((Pointers.block, Pointers.offset)
    Types.prod, Csyntax.type0) Types.prod Types.option -> Csyntax.function0
    -> env -> cont -> 'a1 -> 'a1) -> cont -> 'a1 **)
let rec cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 h_Kswitch h_Kcall = function
| Kstop -> h_Kstop
| Kseq (x_8739, x_8738) ->
  h_Kseq x_8739 x_8738
    (cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
      h_Kswitch h_Kcall x_8738)
| Kwhile (x_8742, x_8741, x_8740) ->
  h_Kwhile x_8742 x_8741 x_8740
    (cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
      h_Kswitch h_Kcall x_8740)
| Kdowhile (x_8745, x_8744, x_8743) ->
  h_Kdowhile x_8745 x_8744 x_8743
    (cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
      h_Kswitch h_Kcall x_8743)
| Kfor2 (x_8749, x_8748, x_8747, x_8746) ->
  h_Kfor2 x_8749 x_8748 x_8747 x_8746
    (cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
      h_Kswitch h_Kcall x_8746)
| Kfor3 (x_8753, x_8752, x_8751, x_8750) ->
  h_Kfor3 x_8753 x_8752 x_8751 x_8750
    (cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
      h_Kswitch h_Kcall x_8750)
| Kswitch x_8754 ->
  h_Kswitch x_8754
    (cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
      h_Kswitch h_Kcall x_8754)
| Kcall (x_8758, x_8757, x_8756, x_8755) ->
  h_Kcall x_8758 x_8757 x_8756 x_8755
    (cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
      h_Kswitch h_Kcall x_8755)

(** val cont_rect_Type3 :
    'a1 -> (Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
    Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
    Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
    Csyntax.statement -> Csyntax.statement -> cont -> 'a1 -> 'a1) ->
    (Csyntax.expr -> Csyntax.statement -> Csyntax.statement -> cont -> 'a1 ->
    'a1) -> (cont -> 'a1 -> 'a1) -> (((Pointers.block, Pointers.offset)
    Types.prod, Csyntax.type0) Types.prod Types.option -> Csyntax.function0
    -> env -> cont -> 'a1 -> 'a1) -> cont -> 'a1 **)
let rec cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 h_Kswitch h_Kcall = function
| Kstop -> h_Kstop
| Kseq (x_8799, x_8798) ->
  h_Kseq x_8799 x_8798
    (cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
      h_Kswitch h_Kcall x_8798)
| Kwhile (x_8802, x_8801, x_8800) ->
  h_Kwhile x_8802 x_8801 x_8800
    (cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
      h_Kswitch h_Kcall x_8800)
| Kdowhile (x_8805, x_8804, x_8803) ->
  h_Kdowhile x_8805 x_8804 x_8803
    (cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
      h_Kswitch h_Kcall x_8803)
| Kfor2 (x_8809, x_8808, x_8807, x_8806) ->
  h_Kfor2 x_8809 x_8808 x_8807 x_8806
    (cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
      h_Kswitch h_Kcall x_8806)
| Kfor3 (x_8813, x_8812, x_8811, x_8810) ->
  h_Kfor3 x_8813 x_8812 x_8811 x_8810
    (cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
      h_Kswitch h_Kcall x_8810)
| Kswitch x_8814 ->
  h_Kswitch x_8814
    (cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
      h_Kswitch h_Kcall x_8814)
| Kcall (x_8818, x_8817, x_8816, x_8815) ->
  h_Kcall x_8818 x_8817 x_8816 x_8815
    (cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
      h_Kswitch h_Kcall x_8815)

(** val cont_rect_Type2 :
    'a1 -> (Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
    Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
    Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
    Csyntax.statement -> Csyntax.statement -> cont -> 'a1 -> 'a1) ->
    (Csyntax.expr -> Csyntax.statement -> Csyntax.statement -> cont -> 'a1 ->
    'a1) -> (cont -> 'a1 -> 'a1) -> (((Pointers.block, Pointers.offset)
    Types.prod, Csyntax.type0) Types.prod Types.option -> Csyntax.function0
    -> env -> cont -> 'a1 -> 'a1) -> cont -> 'a1 **)
let rec cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 h_Kswitch h_Kcall = function
| Kstop -> h_Kstop
| Kseq (x_8829, x_8828) ->
  h_Kseq x_8829 x_8828
    (cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
      h_Kswitch h_Kcall x_8828)
| Kwhile (x_8832, x_8831, x_8830) ->
  h_Kwhile x_8832 x_8831 x_8830
    (cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
      h_Kswitch h_Kcall x_8830)
| Kdowhile (x_8835, x_8834, x_8833) ->
  h_Kdowhile x_8835 x_8834 x_8833
    (cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
      h_Kswitch h_Kcall x_8833)
| Kfor2 (x_8839, x_8838, x_8837, x_8836) ->
  h_Kfor2 x_8839 x_8838 x_8837 x_8836
    (cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
      h_Kswitch h_Kcall x_8836)
| Kfor3 (x_8843, x_8842, x_8841, x_8840) ->
  h_Kfor3 x_8843 x_8842 x_8841 x_8840
    (cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
      h_Kswitch h_Kcall x_8840)
| Kswitch x_8844 ->
  h_Kswitch x_8844
    (cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
      h_Kswitch h_Kcall x_8844)
| Kcall (x_8848, x_8847, x_8846, x_8845) ->
  h_Kcall x_8848 x_8847 x_8846 x_8845
    (cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
      h_Kswitch h_Kcall x_8845)

(** val cont_rect_Type1 :
    'a1 -> (Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
    Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
    Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
    Csyntax.statement -> Csyntax.statement -> cont -> 'a1 -> 'a1) ->
    (Csyntax.expr -> Csyntax.statement -> Csyntax.statement -> cont -> 'a1 ->
    'a1) -> (cont -> 'a1 -> 'a1) -> (((Pointers.block, Pointers.offset)
    Types.prod, Csyntax.type0) Types.prod Types.option -> Csyntax.function0
    -> env -> cont -> 'a1 -> 'a1) -> cont -> 'a1 **)
let rec cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 h_Kswitch h_Kcall = function
| Kstop -> h_Kstop
| Kseq (x_8859, x_8858) ->
  h_Kseq x_8859 x_8858
    (cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
      h_Kswitch h_Kcall x_8858)
| Kwhile (x_8862, x_8861, x_8860) ->
  h_Kwhile x_8862 x_8861 x_8860
    (cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
      h_Kswitch h_Kcall x_8860)
| Kdowhile (x_8865, x_8864, x_8863) ->
  h_Kdowhile x_8865 x_8864 x_8863
    (cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
      h_Kswitch h_Kcall x_8863)
| Kfor2 (x_8869, x_8868, x_8867, x_8866) ->
  h_Kfor2 x_8869 x_8868 x_8867 x_8866
    (cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
      h_Kswitch h_Kcall x_8866)
| Kfor3 (x_8873, x_8872, x_8871, x_8870) ->
  h_Kfor3 x_8873 x_8872 x_8871 x_8870
    (cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
      h_Kswitch h_Kcall x_8870)
| Kswitch x_8874 ->
  h_Kswitch x_8874
    (cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
      h_Kswitch h_Kcall x_8874)
| Kcall (x_8878, x_8877, x_8876, x_8875) ->
  h_Kcall x_8878 x_8877 x_8876 x_8875
    (cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
      h_Kswitch h_Kcall x_8875)

(** val cont_rect_Type0 :
    'a1 -> (Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
    Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
    Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
    Csyntax.statement -> Csyntax.statement -> cont -> 'a1 -> 'a1) ->
    (Csyntax.expr -> Csyntax.statement -> Csyntax.statement -> cont -> 'a1 ->
    'a1) -> (cont -> 'a1 -> 'a1) -> (((Pointers.block, Pointers.offset)
    Types.prod, Csyntax.type0) Types.prod Types.option -> Csyntax.function0
    -> env -> cont -> 'a1 -> 'a1) -> cont -> 'a1 **)
let rec cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 h_Kswitch h_Kcall = function
| Kstop -> h_Kstop
| Kseq (x_8889, x_8888) ->
  h_Kseq x_8889 x_8888
    (cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
      h_Kswitch h_Kcall x_8888)
| Kwhile (x_8892, x_8891, x_8890) ->
  h_Kwhile x_8892 x_8891 x_8890
    (cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
      h_Kswitch h_Kcall x_8890)
| Kdowhile (x_8895, x_8894, x_8893) ->
  h_Kdowhile x_8895 x_8894 x_8893
    (cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
      h_Kswitch h_Kcall x_8893)
| Kfor2 (x_8899, x_8898, x_8897, x_8896) ->
  h_Kfor2 x_8899 x_8898 x_8897 x_8896
    (cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
      h_Kswitch h_Kcall x_8896)
| Kfor3 (x_8903, x_8902, x_8901, x_8900) ->
  h_Kfor3 x_8903 x_8902 x_8901 x_8900
    (cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
      h_Kswitch h_Kcall x_8900)
| Kswitch x_8904 ->
  h_Kswitch x_8904
    (cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
      h_Kswitch h_Kcall x_8904)
| Kcall (x_8908, x_8907, x_8906, x_8905) ->
  h_Kcall x_8908 x_8907 x_8906 x_8905
    (cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
      h_Kswitch h_Kcall x_8905)

(** val cont_inv_rect_Type4 :
    cont -> (__ -> 'a1) -> (Csyntax.statement -> cont -> (__ -> 'a1) -> __ ->
    'a1) -> (Csyntax.expr -> Csyntax.statement -> cont -> (__ -> 'a1) -> __
    -> 'a1) -> (Csyntax.expr -> Csyntax.statement -> cont -> (__ -> 'a1) ->
    __ -> 'a1) -> (Csyntax.expr -> Csyntax.statement -> Csyntax.statement ->
    cont -> (__ -> 'a1) -> __ -> 'a1) -> (Csyntax.expr -> Csyntax.statement
    -> Csyntax.statement -> cont -> (__ -> 'a1) -> __ -> 'a1) -> (cont -> (__
    -> 'a1) -> __ -> 'a1) -> (((Pointers.block, Pointers.offset) Types.prod,
    Csyntax.type0) Types.prod Types.option -> Csyntax.function0 -> env ->
    cont -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 **)
let cont_inv_rect_Type4 hterm h1 h2 h3 h4 h5 h6 h7 h8 =
  let hcut = cont_rect_Type4 h1 h2 h3 h4 h5 h6 h7 h8 hterm in hcut __

(** val cont_inv_rect_Type3 :
    cont -> (__ -> 'a1) -> (Csyntax.statement -> cont -> (__ -> 'a1) -> __ ->
    'a1) -> (Csyntax.expr -> Csyntax.statement -> cont -> (__ -> 'a1) -> __
    -> 'a1) -> (Csyntax.expr -> Csyntax.statement -> cont -> (__ -> 'a1) ->
    __ -> 'a1) -> (Csyntax.expr -> Csyntax.statement -> Csyntax.statement ->
    cont -> (__ -> 'a1) -> __ -> 'a1) -> (Csyntax.expr -> Csyntax.statement
    -> Csyntax.statement -> cont -> (__ -> 'a1) -> __ -> 'a1) -> (cont -> (__
    -> 'a1) -> __ -> 'a1) -> (((Pointers.block, Pointers.offset) Types.prod,
    Csyntax.type0) Types.prod Types.option -> Csyntax.function0 -> env ->
    cont -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 **)
let cont_inv_rect_Type3 hterm h1 h2 h3 h4 h5 h6 h7 h8 =
  let hcut = cont_rect_Type3 h1 h2 h3 h4 h5 h6 h7 h8 hterm in hcut __

(** val cont_inv_rect_Type2 :
    cont -> (__ -> 'a1) -> (Csyntax.statement -> cont -> (__ -> 'a1) -> __ ->
    'a1) -> (Csyntax.expr -> Csyntax.statement -> cont -> (__ -> 'a1) -> __
    -> 'a1) -> (Csyntax.expr -> Csyntax.statement -> cont -> (__ -> 'a1) ->
    __ -> 'a1) -> (Csyntax.expr -> Csyntax.statement -> Csyntax.statement ->
    cont -> (__ -> 'a1) -> __ -> 'a1) -> (Csyntax.expr -> Csyntax.statement
    -> Csyntax.statement -> cont -> (__ -> 'a1) -> __ -> 'a1) -> (cont -> (__
    -> 'a1) -> __ -> 'a1) -> (((Pointers.block, Pointers.offset) Types.prod,
    Csyntax.type0) Types.prod Types.option -> Csyntax.function0 -> env ->
    cont -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 **)
let cont_inv_rect_Type2 hterm h1 h2 h3 h4 h5 h6 h7 h8 =
  let hcut = cont_rect_Type2 h1 h2 h3 h4 h5 h6 h7 h8 hterm in hcut __

(** val cont_inv_rect_Type1 :
    cont -> (__ -> 'a1) -> (Csyntax.statement -> cont -> (__ -> 'a1) -> __ ->
    'a1) -> (Csyntax.expr -> Csyntax.statement -> cont -> (__ -> 'a1) -> __
    -> 'a1) -> (Csyntax.expr -> Csyntax.statement -> cont -> (__ -> 'a1) ->
    __ -> 'a1) -> (Csyntax.expr -> Csyntax.statement -> Csyntax.statement ->
    cont -> (__ -> 'a1) -> __ -> 'a1) -> (Csyntax.expr -> Csyntax.statement
    -> Csyntax.statement -> cont -> (__ -> 'a1) -> __ -> 'a1) -> (cont -> (__
    -> 'a1) -> __ -> 'a1) -> (((Pointers.block, Pointers.offset) Types.prod,
    Csyntax.type0) Types.prod Types.option -> Csyntax.function0 -> env ->
    cont -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 **)
let cont_inv_rect_Type1 hterm h1 h2 h3 h4 h5 h6 h7 h8 =
  let hcut = cont_rect_Type1 h1 h2 h3 h4 h5 h6 h7 h8 hterm in hcut __

(** val cont_inv_rect_Type0 :
    cont -> (__ -> 'a1) -> (Csyntax.statement -> cont -> (__ -> 'a1) -> __ ->
    'a1) -> (Csyntax.expr -> Csyntax.statement -> cont -> (__ -> 'a1) -> __
    -> 'a1) -> (Csyntax.expr -> Csyntax.statement -> cont -> (__ -> 'a1) ->
    __ -> 'a1) -> (Csyntax.expr -> Csyntax.statement -> Csyntax.statement ->
    cont -> (__ -> 'a1) -> __ -> 'a1) -> (Csyntax.expr -> Csyntax.statement
    -> Csyntax.statement -> cont -> (__ -> 'a1) -> __ -> 'a1) -> (cont -> (__
    -> 'a1) -> __ -> 'a1) -> (((Pointers.block, Pointers.offset) Types.prod,
    Csyntax.type0) Types.prod Types.option -> Csyntax.function0 -> env ->
    cont -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 **)
let cont_inv_rect_Type0 hterm h1 h2 h3 h4 h5 h6 h7 h8 =
  let hcut = cont_rect_Type0 h1 h2 h3 h4 h5 h6 h7 h8 hterm in hcut __

(** val cont_discr : cont -> cont -> __ **)
let cont_discr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | Kstop -> Obj.magic (fun _ dH -> dH)
     | Kseq (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
     | Kwhile (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
     | Kdowhile (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
     | Kfor2 (a0, a1, a2, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
     | Kfor3 (a0, a1, a2, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
     | Kswitch a0 -> Obj.magic (fun _ dH -> dH __)
     | Kcall (a0, a1, a2, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)) y

(** val cont_jmdiscr : cont -> cont -> __ **)
let cont_jmdiscr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | Kstop -> Obj.magic (fun _ dH -> dH)
     | Kseq (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
     | Kwhile (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
     | Kdowhile (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
     | Kfor2 (a0, a1, a2, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
     | Kfor3 (a0, a1, a2, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
     | Kswitch a0 -> Obj.magic (fun _ dH -> dH __)
     | Kcall (a0, a1, a2, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)) y

(** val call_cont : cont -> cont **)
let rec call_cont k = match k with
| Kstop -> k
| Kseq (s, k0) -> call_cont k0
| Kwhile (e, s, k0) -> call_cont k0
| Kdowhile (e, s, k0) -> call_cont k0
| Kfor2 (e2, e3, s, k0) -> call_cont k0
| Kfor3 (e2, e3, s, k0) -> call_cont k0
| Kswitch k0 -> call_cont k0
| Kcall (x, x0, x1, x2) -> k

type state =
| State of Csyntax.function0 * Csyntax.statement * cont * env * GenMem.mem
| Callstate of AST.ident * Csyntax.clight_fundef * Values.val0 List.list
   * cont * GenMem.mem
| Returnstate of Values.val0 * cont * GenMem.mem
| Finalstate of Integers.int

(** val state_rect_Type4 :
    (Csyntax.function0 -> Csyntax.statement -> cont -> env -> GenMem.mem ->
    'a1) -> (AST.ident -> Csyntax.clight_fundef -> Values.val0 List.list ->
    cont -> GenMem.mem -> 'a1) -> (Values.val0 -> cont -> GenMem.mem -> 'a1)
    -> (Integers.int -> 'a1) -> state -> 'a1 **)
let rec state_rect_Type4 h_State h_Callstate h_Returnstate h_Finalstate = function
| State (f, s, k, e, m) -> h_State f s k e m
| Callstate (id, fd, args, k, m) -> h_Callstate id fd args k m
| Returnstate (res, k, m) -> h_Returnstate res k m
| Finalstate r -> h_Finalstate r

(** val state_rect_Type5 :
    (Csyntax.function0 -> Csyntax.statement -> cont -> env -> GenMem.mem ->
    'a1) -> (AST.ident -> Csyntax.clight_fundef -> Values.val0 List.list ->
    cont -> GenMem.mem -> 'a1) -> (Values.val0 -> cont -> GenMem.mem -> 'a1)
    -> (Integers.int -> 'a1) -> state -> 'a1 **)
let rec state_rect_Type5 h_State h_Callstate h_Returnstate h_Finalstate = function
| State (f, s, k, e, m) -> h_State f s k e m
| Callstate (id, fd, args, k, m) -> h_Callstate id fd args k m
| Returnstate (res, k, m) -> h_Returnstate res k m
| Finalstate r -> h_Finalstate r

(** val state_rect_Type3 :
    (Csyntax.function0 -> Csyntax.statement -> cont -> env -> GenMem.mem ->
    'a1) -> (AST.ident -> Csyntax.clight_fundef -> Values.val0 List.list ->
    cont -> GenMem.mem -> 'a1) -> (Values.val0 -> cont -> GenMem.mem -> 'a1)
    -> (Integers.int -> 'a1) -> state -> 'a1 **)
let rec state_rect_Type3 h_State h_Callstate h_Returnstate h_Finalstate = function
| State (f, s, k, e, m) -> h_State f s k e m
| Callstate (id, fd, args, k, m) -> h_Callstate id fd args k m
| Returnstate (res, k, m) -> h_Returnstate res k m
| Finalstate r -> h_Finalstate r

(** val state_rect_Type2 :
    (Csyntax.function0 -> Csyntax.statement -> cont -> env -> GenMem.mem ->
    'a1) -> (AST.ident -> Csyntax.clight_fundef -> Values.val0 List.list ->
    cont -> GenMem.mem -> 'a1) -> (Values.val0 -> cont -> GenMem.mem -> 'a1)
    -> (Integers.int -> 'a1) -> state -> 'a1 **)
let rec state_rect_Type2 h_State h_Callstate h_Returnstate h_Finalstate = function
| State (f, s, k, e, m) -> h_State f s k e m
| Callstate (id, fd, args, k, m) -> h_Callstate id fd args k m
| Returnstate (res, k, m) -> h_Returnstate res k m
| Finalstate r -> h_Finalstate r

(** val state_rect_Type1 :
    (Csyntax.function0 -> Csyntax.statement -> cont -> env -> GenMem.mem ->
    'a1) -> (AST.ident -> Csyntax.clight_fundef -> Values.val0 List.list ->
    cont -> GenMem.mem -> 'a1) -> (Values.val0 -> cont -> GenMem.mem -> 'a1)
    -> (Integers.int -> 'a1) -> state -> 'a1 **)
let rec state_rect_Type1 h_State h_Callstate h_Returnstate h_Finalstate = function
| State (f, s, k, e, m) -> h_State f s k e m
| Callstate (id, fd, args, k, m) -> h_Callstate id fd args k m
| Returnstate (res, k, m) -> h_Returnstate res k m
| Finalstate r -> h_Finalstate r

(** val state_rect_Type0 :
    (Csyntax.function0 -> Csyntax.statement -> cont -> env -> GenMem.mem ->
    'a1) -> (AST.ident -> Csyntax.clight_fundef -> Values.val0 List.list ->
    cont -> GenMem.mem -> 'a1) -> (Values.val0 -> cont -> GenMem.mem -> 'a1)
    -> (Integers.int -> 'a1) -> state -> 'a1 **)
let rec state_rect_Type0 h_State h_Callstate h_Returnstate h_Finalstate = function
| State (f, s, k, e, m) -> h_State f s k e m
| Callstate (id, fd, args, k, m) -> h_Callstate id fd args k m
| Returnstate (res, k, m) -> h_Returnstate res k m
| Finalstate r -> h_Finalstate r

(** val state_inv_rect_Type4 :
    state -> (Csyntax.function0 -> Csyntax.statement -> cont -> env ->
    GenMem.mem -> __ -> 'a1) -> (AST.ident -> Csyntax.clight_fundef ->
    Values.val0 List.list -> cont -> GenMem.mem -> __ -> 'a1) -> (Values.val0
    -> cont -> GenMem.mem -> __ -> 'a1) -> (Integers.int -> __ -> 'a1) -> 'a1 **)
let state_inv_rect_Type4 hterm h1 h2 h3 h4 =
  let hcut = state_rect_Type4 h1 h2 h3 h4 hterm in hcut __

(** val state_inv_rect_Type3 :
    state -> (Csyntax.function0 -> Csyntax.statement -> cont -> env ->
    GenMem.mem -> __ -> 'a1) -> (AST.ident -> Csyntax.clight_fundef ->
    Values.val0 List.list -> cont -> GenMem.mem -> __ -> 'a1) -> (Values.val0
    -> cont -> GenMem.mem -> __ -> 'a1) -> (Integers.int -> __ -> 'a1) -> 'a1 **)
let state_inv_rect_Type3 hterm h1 h2 h3 h4 =
  let hcut = state_rect_Type3 h1 h2 h3 h4 hterm in hcut __

(** val state_inv_rect_Type2 :
    state -> (Csyntax.function0 -> Csyntax.statement -> cont -> env ->
    GenMem.mem -> __ -> 'a1) -> (AST.ident -> Csyntax.clight_fundef ->
    Values.val0 List.list -> cont -> GenMem.mem -> __ -> 'a1) -> (Values.val0
    -> cont -> GenMem.mem -> __ -> 'a1) -> (Integers.int -> __ -> 'a1) -> 'a1 **)
let state_inv_rect_Type2 hterm h1 h2 h3 h4 =
  let hcut = state_rect_Type2 h1 h2 h3 h4 hterm in hcut __

(** val state_inv_rect_Type1 :
    state -> (Csyntax.function0 -> Csyntax.statement -> cont -> env ->
    GenMem.mem -> __ -> 'a1) -> (AST.ident -> Csyntax.clight_fundef ->
    Values.val0 List.list -> cont -> GenMem.mem -> __ -> 'a1) -> (Values.val0
    -> cont -> GenMem.mem -> __ -> 'a1) -> (Integers.int -> __ -> 'a1) -> 'a1 **)
let state_inv_rect_Type1 hterm h1 h2 h3 h4 =
  let hcut = state_rect_Type1 h1 h2 h3 h4 hterm in hcut __

(** val state_inv_rect_Type0 :
    state -> (Csyntax.function0 -> Csyntax.statement -> cont -> env ->
    GenMem.mem -> __ -> 'a1) -> (AST.ident -> Csyntax.clight_fundef ->
    Values.val0 List.list -> cont -> GenMem.mem -> __ -> 'a1) -> (Values.val0
    -> cont -> GenMem.mem -> __ -> 'a1) -> (Integers.int -> __ -> 'a1) -> 'a1 **)
let state_inv_rect_Type0 hterm h1 h2 h3 h4 =
  let hcut = state_rect_Type0 h1 h2 h3 h4 hterm in hcut __

(** val state_discr : state -> state -> __ **)
let state_discr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | State (a0, a1, a2, a3, a4) ->
       Obj.magic (fun _ dH -> dH __ __ __ __ __)
     | Callstate (a0, a1, a2, a3, a4) ->
       Obj.magic (fun _ dH -> dH __ __ __ __ __)
     | Returnstate (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
     | Finalstate a0 -> Obj.magic (fun _ dH -> dH __)) y

(** val state_jmdiscr : state -> state -> __ **)
let state_jmdiscr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | State (a0, a1, a2, a3, a4) ->
       Obj.magic (fun _ dH -> dH __ __ __ __ __)
     | Callstate (a0, a1, a2, a3, a4) ->
       Obj.magic (fun _ dH -> dH __ __ __ __ __)
     | Returnstate (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
     | Finalstate a0 -> Obj.magic (fun _ dH -> dH __)) y

(** val find_label :
    Csyntax.label -> Csyntax.statement -> cont -> (Csyntax.statement, cont)
    Types.prod Types.option **)
let rec find_label lbl s k =
  match s with
  | Csyntax.Sskip -> Types.None
  | Csyntax.Sassign (x, x0) -> Types.None
  | Csyntax.Scall (x, x0, x1) -> Types.None
  | Csyntax.Ssequence (s1, s2) ->
    (match find_label lbl s1 (Kseq (s2, k)) with
     | Types.None -> find_label lbl s2 k
     | Types.Some sk -> Types.Some sk)
  | Csyntax.Sifthenelse (a, s1, s2) ->
    (match find_label lbl s1 k with
     | Types.None -> find_label lbl s2 k
     | Types.Some sk -> Types.Some sk)
  | Csyntax.Swhile (a, s1) -> find_label lbl s1 (Kwhile (a, s1, k))
  | Csyntax.Sdowhile (a, s1) -> find_label lbl s1 (Kdowhile (a, s1, k))
  | Csyntax.Sfor (a1, a2, a3, s1) ->
    (match find_label lbl a1 (Kseq ((Csyntax.Sfor (Csyntax.Sskip, a2, a3,
             s1)), k)) with
     | Types.None ->
       (match find_label lbl s1 (Kfor2 (a2, a3, s1, k)) with
        | Types.None -> find_label lbl a3 (Kfor3 (a2, a3, s1, k))
        | Types.Some sk -> Types.Some sk)
     | Types.Some sk -> Types.Some sk)
  | Csyntax.Sbreak -> Types.None
  | Csyntax.Scontinue -> Types.None
  | Csyntax.Sreturn x -> Types.None
  | Csyntax.Sswitch (e, sl) -> find_label_ls lbl sl (Kswitch k)
  | Csyntax.Slabel (lbl', s') ->
    (match AST.ident_eq lbl lbl' with
     | Types.Inl _ -> Types.Some { Types.fst = s'; Types.snd = k }
     | Types.Inr _ -> find_label lbl s' k)
  | Csyntax.Sgoto x -> Types.None
  | Csyntax.Scost (c, s') -> find_label lbl s' k
(** val find_label_ls :
    Csyntax.label -> Csyntax.labeled_statements -> cont ->
    (Csyntax.statement, cont) Types.prod Types.option **)
and find_label_ls lbl sl k =
  match sl with
  | Csyntax.LSdefault s -> find_label lbl s k
  | Csyntax.LScase (x, x0, s, sl') ->
    (match find_label lbl s (Kseq ((seq_of_labeled_statement sl'), k)) with
     | Types.None -> find_label_ls lbl sl' k
     | Types.Some sk -> Types.Some sk)

(** val fun_typeof : Csyntax.expr -> Csyntax.type0 **)
let fun_typeof e =
  match Csyntax.typeof e with
  | Csyntax.Tvoid -> Csyntax.Tvoid
  | Csyntax.Tint (a, b) -> Csyntax.Tint (a, b)
  | Csyntax.Tpointer ty -> ty
  | Csyntax.Tarray (a, b) -> Csyntax.Tarray (a, b)
  | Csyntax.Tfunction (a, b) -> Csyntax.Tfunction (a, b)
  | Csyntax.Tstruct (a, b) -> Csyntax.Tstruct (a, b)
  | Csyntax.Tunion (a, b) -> Csyntax.Tunion (a, b)
  | Csyntax.Tcomp_ptr a -> Csyntax.Tcomp_ptr a