Require Import VST.floyd.proofauto.
Require Import VST.progs.int_or_ptr.
Instance CompSpecs : compspecs. make_compspecs prog. Defined.
Definition Vprog : varspecs. mk_varspecs prog. Defined.

Inductive tree := 
| LEAF: forall i, 0 <= i <= Int.max_signed -> tree
| NODE: tree -> tree -> tree.

Fixpoint treerep (t: tree) (p: val) : mpred :=
  match t with
  | LEAF i _ => !! (p = Vint (Int.repr (i+i+1))) && emp
  | NODE t1 t2 => EX p1:val, EX p2: val,
               data_at Tsh (Tstruct _tree noattr) (p1,p2) p
              * treerep t1 p1 * treerep t2 p2
  end.

Definition POINTER_BOUNDARY : Z := 1024.

Definition valid_int_or_ptr (x: val) :=
 match x with
 | Vint i => Int.testbit i 0 = true
              \/ Int.unsigned i < POINTER_BOUNDARY
 | Vptr b z => Ptrofs.testbit z 0 = false
 | _ => False
 end.

Lemma valid_int_or_ptr_ii1:
 forall i, valid_int_or_ptr (Vint (Int.repr (i + i + 1))).
Proof.
(* Goal: forall (t : tree) (p : val), @derives mpred Nveric (treerep t p) (@prop mpred Nveric (valid_int_or_ptr p)) *)
intros.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Tsh (Tstruct _tree noattr) (@pair val val p1 p2) r) (treerep t2 q)) (treerep t2 p2)) (treerep t1 p)) (treerep t1 p1)) (@data_at CompSpecs Tsh (Tstruct _tree noattr) (@pair val val p q) (Vptr b i))) (@exp mpred Nveric val (fun a : val => @andp mpred Nveric (@prop mpred Nveric (@eq val r a)) (@sepcon mpred Nveric Sveric (treerep (NODE t1 t2) (Vptr b i)) (treerep (NODE t1 t2) a)))) *)
simpl.
(* Goal: or (@eq bool (Z.odd (Int.unsigned (Int.repr (Z.add (Z.add i i) (Zpos xH))))) true) (Z.lt (Int.unsigned (Int.repr (Z.add (Z.add i i) (Zpos xH)))) POINTER_BOUNDARY) *)
left.
(* Goal: @eq bool (Z.odd (Int.unsigned (Int.repr (Z.add (Z.add i i) (Zpos xH))))) true *)
rewrite Int.unsigned_repr_eq.
(* Goal: @eq bool (Z.odd (Z.modulo (Z.add (Z.add i i) (Zpos xH)) Int.modulus)) true *)
rewrite Zodd_mod.
(* Goal: @eq bool (Zeq_bool (Z.modulo (Z.modulo (Z.add (Z.add i i) (Zpos xH)) Int.modulus) (Zpos (xO xH))) (Zpos xH)) true *)
apply Zeq_is_eq_bool.
(* Goal: @eq Z (Z.modulo (Z.modulo (Z.add (Z.add i i) (Zpos xH)) Int.modulus) (Zpos (xO xH))) (Zpos xH) *)
replace (i+i) with (2*i)%Z by omega.
(* Goal: @eq Z (Z.modulo (Z.modulo (Z.add (Z.mul (Zpos (xO xH)) i) (Zpos xH)) Int.modulus) (Zpos (xO xH))) (Zpos xH) *)
rewrite <- Zmod_div_mod; try omega.
(* Goal: @eq Z (Z.modulo (Z.add (Z.mul (Zpos (xO xH)) i) (Zpos xH)) (Zpos (xO xH))) (Zpos xH) *)
(* Goal: Z.lt Z0 Int.modulus *)
(* Goal: Z.divide (Zpos (xO xH)) Int.modulus *)
rewrite Z.mul_comm, Z.add_comm.
(* Goal: @eq Z (Z.modulo (Z.add (Zpos xH) (Z.mul i (Zpos (xO xH)))) (Zpos (xO xH))) (Zpos xH) *)
(* Goal: Z.lt Z0 Int.modulus *)
(* Goal: Z.divide (Zpos (xO xH)) Int.modulus *)
rewrite Z_mod_plus_full.
(* Goal: @eq Z Int.modulus (Z.mul (Z.div Int.modulus (Zpos (xO xH))) (Zpos (xO xH))) *)
reflexivity.
(* Goal: @eq Z Int.modulus (Z.mul (Z.div Int.modulus (Zpos (xO xH))) (Zpos (xO xH))) *)
compute; reflexivity.
(* Goal: Z.divide (Zpos (xO xH)) Int.modulus *)
exists (Z.div Int.modulus 2).
(* Goal: @eq Z Int.modulus (Z.mul (Z.div Int.modulus (Zpos (xO xH))) (Zpos (xO xH))) *)
reflexivity.
Qed.


Lemma valid_int_or_ptr_i2:
 forall i, 0 <= i < POINTER_BOUNDARY ->
   valid_int_or_ptr (Vint (Int.repr i)).
Proof.
(* Goal: forall (t : tree) (p : val), @derives mpred Nveric (treerep t p) (@prop mpred Nveric (valid_int_or_ptr p)) *)
intros.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Tsh (Tstruct _tree noattr) (@pair val val p1 p2) r) (treerep t2 q)) (treerep t2 p2)) (treerep t1 p)) (treerep t1 p1)) (@data_at CompSpecs Tsh (Tstruct _tree noattr) (@pair val val p q) (Vptr b i))) (@exp mpred Nveric val (fun a : val => @andp mpred Nveric (@prop mpred Nveric (@eq val r a)) (@sepcon mpred Nveric Sveric (treerep (NODE t1 t2) (Vptr b i)) (treerep (NODE t1 t2) a)))) *)
simpl.
right.
unfold POINTER_BOUNDARY in *.
rewrite Int.unsigned_repr by rep_omega.
rep_omega.
Qed.

Lemma field_compatible_valid_int_or_ptr:
  forall p, 
  field_compatible (Tstruct _tree noattr) [] p ->
  valid_int_or_ptr p.
Proof.
(* Goal: forall (t : tree) (p : val), @derives mpred Nveric (treerep t p) (@prop mpred Nveric (valid_int_or_ptr p)) *)
intros.
(* Goal: valid_int_or_ptr p *)
destruct H as [H1 [_ [_ [H2 _]]]].
(* Goal: valid_int_or_ptr p *)
destruct p; try contradiction.
(* Goal: valid_int_or_ptr (Vptr b i) *)
clear - H2; simpl in *.
(* Goal: @eq bool (Z.odd (Ptrofs.unsigned i)) false *)
    rewrite Zodd_even_bool.
(* Goal: @eq bool (negb (Z.even (Ptrofs.unsigned i))) false *)
    apply negb_false_iff.
(* Goal: @eq bool (Z.even (Ptrofs.unsigned i)) true *)
    apply Zeven_bool_iff.
(* Goal: Zeven (Ptrofs.unsigned i) *)
    inv H2.
(* Goal: Zeven (Ptrofs.unsigned i) *)
(* Goal: Zeven (Ptrofs.unsigned i) *)
    1: inv H.
(* Goal: Zeven (Ptrofs.unsigned i) *)
    inv H1.
(* Goal: Zeven (Ptrofs.unsigned i) *)
    specialize (H4 _left _ _ eq_refl eq_refl).
(* Goal: Zeven (Ptrofs.unsigned i) *)
    inv H4.
(* Goal: Zeven (Ptrofs.unsigned i) *)
    inv H.
(* Goal: Zeven (Ptrofs.unsigned i) *)
    simpl in H0.
(* Goal: Zeven (Ptrofs.unsigned i) *)
    destruct H0 as [j H].
(* Goal: Zeven (Ptrofs.unsigned i) *)
    rewrite Z.add_0_r in H.
(* Goal: Zeven (Ptrofs.unsigned i) *)
    rewrite H; clear.
(* Goal: Zeven (Z.mul j (Zpos (xO (xO xH)))) *)
    replace (j*4)%Z with (2*(2*j))%Z by omega.
(* Goal: Zeven (Z.mul (Zpos (xO xH)) (Z.mul (Zpos (xO xH)) j)) *)
    apply Zeven_2p.
Qed.

Lemma treerep_local_facts:
  forall t p,
   treerep t p |--
   !! (valid_int_or_ptr p).
Proof.
(* Goal: forall (t : tree) (p : val), @derives mpred Nveric (treerep t p) (@prop mpred Nveric (valid_int_or_ptr p)) *)
intros.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Tsh (Tstruct _tree noattr) (@pair val val p1 p2) r) (treerep t2 q)) (treerep t2 p2)) (treerep t1 p)) (treerep t1 p1)) (@data_at CompSpecs Tsh (Tstruct _tree noattr) (@pair val val p q) (Vptr b i))) (@exp mpred Nveric val (fun a : val => @andp mpred Nveric (@prop mpred Nveric (@eq val r a)) (@sepcon mpred Nveric Sveric (treerep (NODE t1 t2) (Vptr b i)) (treerep (NODE t1 t2) a)))) *)
destruct t; simpl.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Tsh (Tstruct _tree noattr) (@pair val val p1 p2) r) (treerep t2 q)) (treerep t2 p2)) (treerep t1 p)) (treerep t1 p1)) (@data_at CompSpecs Tsh (Tstruct _tree noattr) (@pair val val p q) (Vptr b i))) (@andp mpred Nveric (@prop mpred Nveric (@eq val r r)) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Tsh (Tstruct _tree noattr) (@pair val val p q) (Vptr b i)) (treerep t1 p)) (treerep t2 q)) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Tsh (Tstruct _tree noattr) (@pair val val p1 p2) r) (treerep t1 p1)) (treerep t2 p2)))) *)
entailer!.
(* Goal: valid_int_or_ptr (Vint (Int.repr (Z.add (Z.add i i) (Zpos xH)))) *)
(* Goal: @derives mpred Nveric (@exp mpred Nveric val (fun p1 : val => @exp mpred Nveric val (fun p2 : val => @sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Tsh (Tstruct _tree noattr) (@pair val val p1 p2) p) (treerep t1 p1)) (treerep t2 p2)))) (@prop mpred Nveric (valid_int_or_ptr p)) *)
apply valid_int_or_ptr_ii1.
(* Goal: @derives mpred Nveric (@exp mpred Nveric val (fun p1 : val => @exp mpred Nveric val (fun p2 : val => @sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Tsh (Tstruct _tree noattr) (@pair val val p1 p2) p) (treerep t1 p1)) (treerep t2 p2)))) (@prop mpred Nveric (valid_int_or_ptr p)) *)
Intros p1 p2.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Tsh (Tstruct _tree noattr) (@pair val val p1 p2) r) (treerep t2 q)) (treerep t2 p2)) (treerep t1 p)) (treerep t1 p1)) (@data_at CompSpecs Tsh (Tstruct _tree noattr) (@pair val val p q) (Vptr b i))) (@andp mpred Nveric (@prop mpred Nveric (@eq val r r)) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Tsh (Tstruct _tree noattr) (@pair val val p q) (Vptr b i)) (treerep t1 p)) (treerep t2 q)) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Tsh (Tstruct _tree noattr) (@pair val val p1 p2) r) (treerep t1 p1)) (treerep t2 p2)))) *)
entailer!.
(* Goal: valid_int_or_ptr r *)
apply field_compatible_valid_int_or_ptr; auto.
Qed.

Hint Resolve treerep_local_facts : saturate_local.

Definition test_int_or_ptr_spec :=
 DECLARE _test_int_or_ptr
 WITH x : val
 PRE [ _x OF int_or_ptr_type ]
   PROP(valid_int_or_ptr x) LOCAL(temp _x x) SEP()
 POST [ tint ]
   PROP() 
   LOCAL(temp ret_temp 
          (Vint (Int.repr (match x with
                    | Vint _ => 1
                    | _ => 0
                    end))))
   SEP().

Definition int_or_ptr_to_int_spec :=
 DECLARE _int_or_ptr_to_int
 WITH x : val
 PRE [ _x OF int_or_ptr_type ]
   PROP(is_int I32 Signed x) LOCAL(temp _x x) SEP()
 POST [ tint ]
   PROP() LOCAL (temp ret_temp x) SEP().

Definition int_or_ptr_to_ptr_spec :=
 DECLARE _int_or_ptr_to_ptr
 WITH x : val
 PRE [ _x OF int_or_ptr_type ]
   PROP(isptr x) LOCAL(temp _x x) SEP()
 POST [ tptr tvoid ]
   PROP() LOCAL (temp ret_temp x) SEP().

Definition int_to_int_or_ptr_spec :=
 DECLARE _int_to_int_or_ptr
 WITH x : val
 PRE [ _x OF tint ]
   PROP(valid_int_or_ptr x)
   LOCAL(temp _x x) SEP()
 POST [ int_or_ptr_type ]
   PROP() LOCAL (temp ret_temp x) SEP().

Definition ptr_to_int_or_ptr_spec :=
 DECLARE _ptr_to_int_or_ptr
 WITH x : val
 PRE [ _x OF tptr tvoid ]
   PROP(valid_int_or_ptr x) LOCAL(temp _x x) SEP()
 POST [ int_or_ptr_type ]
   PROP() LOCAL (temp ret_temp x) SEP().

Definition makenode_spec :=
 DECLARE _makenode 
  WITH p: val, q: val
  PRE [ _left OF int_or_ptr_type, _right OF int_or_ptr_type ]
    PROP() LOCAL(temp _left p; temp _right q) SEP()
  POST [ tptr (Tstruct _tree noattr) ]
    EX r:val, 
    PROP() LOCAL(temp ret_temp r) 
    SEP (data_at Tsh (Tstruct _tree noattr) (p,q) r).

Definition copytree_spec :=
 DECLARE _copytree
  WITH t: tree, p : val
  PRE  [ _t OF int_or_ptr_type ]
    PROP() LOCAL(temp _t p) SEP (treerep t p)
  POST [ int_or_ptr_type ]
    EX v:val,
    PROP() LOCAL(temp ret_temp v) 
    SEP (treerep t p; treerep t v).

Definition Gprog : funspecs :=
    ltac:(with_library prog [
    test_int_or_ptr_spec;
    int_or_ptr_to_int_spec;
    int_or_ptr_to_ptr_spec;
    int_to_int_or_ptr_spec;
    ptr_to_int_or_ptr_spec;
    makenode_spec; copytree_spec
  ]).

Lemma body_copytree: semax_body Vprog Gprog f_copytree copytree_spec.
Proof.
(* Goal: semax_body Vprog Gprog CompSpecs f_copytree copytree_spec *)
  start_function.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Tsh (Tstruct _tree noattr) (@pair val val p1 p2) r) (treerep t2 q)) (treerep t2 p2)) (treerep t1 p)) (treerep t1 p1)) (@data_at CompSpecs Tsh (Tstruct _tree noattr) (@pair val val p q) (Vptr b i))) (@andp mpred Nveric (@prop mpred Nveric (@eq val r r)) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Tsh (Tstruct _tree noattr) (@pair val val p q) (Vptr b i)) (treerep t1 p)) (treerep t2 q)) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Tsh (Tstruct _tree noattr) (@pair val val p1 p2) r) (treerep t1 p1)) (treerep t2 p2)))) *)
  assert_PROP (valid_int_or_ptr p) by entailer!.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _t p) (@nil localdef)) (SEPx (@cons mpred (treerep t p) (@nil mpred))))) (Ssequence (Scall (@Some ident _t'6) (Evar _test_int_or_ptr (Tfunction (Tcons (Tpointer tvoid (mk_attr false (@Some N (Npos (xO xH))))) Tnil) tint cc_default)) (@cons expr (Etempvar _t (Tpointer tvoid (mk_attr false (@Some N (Npos (xO xH)))))) (@nil expr))) MORE_COMMANDS) POSTCONDITION *)
  destruct t.
* (* LEAF *)
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _t p) (@nil localdef)) (SEPx (@cons mpred (treerep (LEAF i a) p) (@nil mpred))))) (Ssequence (Scall (@Some ident _t'6) (Evar _test_int_or_ptr (Tfunction (Tcons (Tpointer tvoid (mk_attr false (@Some N (Npos (xO xH))))) Tnil) tint cc_default)) (@cons expr (Etempvar _t (Tpointer tvoid (mk_attr false (@Some N (Npos (xO xH)))))) (@nil expr))) MORE_COMMANDS) POSTCONDITION *)
 unfold treerep.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _t p) (@nil localdef)) (SEPx (@cons mpred (@andp mpred Nveric (@prop mpred Nveric (@eq val p (Vint (Int.repr (Z.add (Z.add i i) (Zpos xH)))))) (@emp mpred Nveric Sveric)) (@nil mpred))))) (Ssequence (Scall (@Some ident _t'6) (Evar _test_int_or_ptr (Tfunction (Tcons (Tpointer tvoid (mk_attr false (@Some N (Npos (xO xH))))) Tnil) tint cc_default)) (@cons expr (Etempvar _t (Tpointer tvoid (mk_attr false (@Some N (Npos (xO xH)))))) (@nil expr))) MORE_COMMANDS) POSTCONDITION *)
 Intros. subst p.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _t (Vint (Int.repr (Z.add (Z.add i i) (Zpos xH))))) (@nil localdef)) (SEPx (@cons mpred (@emp mpred Nveric Sveric) (@nil mpred))))) (Ssequence (Scall (@Some ident _t'6) (Evar _test_int_or_ptr (Tfunction (Tcons (Tpointer tvoid (mk_attr false (@Some N (Npos (xO xH))))) Tnil) tint cc_default)) (@cons expr (Etempvar _t (Tpointer tvoid (mk_attr false (@Some N (Npos (xO xH)))))) (@nil expr))) MORE_COMMANDS) POSTCONDITION *)
 forward_call (Vint (Int.repr (i+i+1))).
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _t'6 (Vint (Int.repr Z0))) (@cons localdef (temp _t (Vptr b i)) (@nil localdef))) (SEPx (@cons mpred (@data_at CompSpecs Tsh (Tstruct _tree noattr) (@pair val val p q) (Vptr b i)) (@cons mpred (treerep t1 p) (@cons mpred (treerep t2 q) (@nil mpred))))))) (Sifthenelse (Etempvar _t'6 tint) (Sreturn (@Some expr (Etempvar _t (Tpointer tvoid (mk_attr false (@Some N (Npos (xO xH)))))))) (Ssequence (Ssequence (Scall (@Some ident _t'1) (Evar _int_or_ptr_to_ptr (Tfunction (Tcons (Tpointer tvoid (mk_attr false (@Some N (Npos (xO xH))))) Tnil) (tptr tvoid) cc_default)) (@cons expr (Etempvar _t (Tpointer tvoid (mk_attr false (@Some N (Npos (xO xH)))))) (@nil expr))) (Sset _s (Ecast (Etempvar _t'1 (tptr tvoid)) (tptr (Tstruct _tree noattr))))) (Ssequence (Ssequence (Ssequence (Sset _t'8 (Efield (Ederef (Etempvar _s (tptr (Tstruct _tree noattr))) (Tstruct _tree noattr)) _left (Tpointer tvoid (mk_attr false (@Some N (Npos (xO xH))))))) (Scall (@Some ident _t'2) (Evar _copytree (Tfunction (Tcons (Tpointer tvoid (mk_attr false (@Some N (Npos (xO xH))))) Tnil) (Tpointer tvoid (mk_attr false (@Some N (Npos (xO xH))))) cc_default)) (@cons expr (Etempvar _t'8 (Tpointer tvoid (mk_attr false (@Some N (Npos (xO xH)))))) (@nil expr)))) (Sset _p (Etempvar _t'2 (Tpointer tvoid (mk_attr false (@Some N (Npos (xO xH)))))))) (Ssequence (Ssequence (Ssequence (Sset _t'7 (Efield (Ederef (Etempvar _s (tptr (Tstruct _tree noattr))) (Tstruct _tree noattr)) _right (Tpointer tvoid (mk_attr false (@Some N (Npos (xO xH))))))) (Scall (@Some ident _t'3) (Evar _copytree (Tfunction (Tcons (Tpointer tvoid (mk_attr false (@Some N (Npos (xO xH))))) Tnil) (Tpointer tvoid (mk_attr false (@Some N (Npos (xO xH))))) cc_default)) (@cons expr (Etempvar _t'7 (Tpointer tvoid (mk_attr false (@Some N (Npos (xO xH)))))) (@nil expr)))) (Sset _q (Etempvar _t'3 (Tpointer tvoid (mk_attr false (@Some N (Npos (xO xH)))))))) (Ssequence (Ssequence (Scall (@Some ident _t'4) (Evar _makenode (Tfunction (Tcons (Tpointer tvoid (mk_attr false (@Some N (Npos (xO xH))))) (Tcons (Tpointer tvoid (mk_attr false (@Some N (Npos (xO xH))))) Tnil)) (tptr (Tstruct _tree noattr)) cc_default)) (@cons expr (Etempvar _p (Tpointer tvoid (mk_attr false (@Some N (Npos (xO xH)))))) (@cons expr (Etempvar _q (Tpointer tvoid (mk_attr false (@Some N (Npos (xO xH)))))) (@nil expr)))) (Scall (@Some ident _t'5) (Evar _ptr_to_int_or_ptr (Tfunction (Tcons (tptr tvoid) Tnil) (Tpointer tvoid (mk_attr false (@Some N (Npos (xO xH))))) cc_default)) (@cons expr (Etempvar _t'4 (tptr (Tstruct _tree noattr))) (@nil expr)))) (Sreturn (@Some expr (Etempvar _t'5 (Tpointer tvoid (mk_attr false (@Some N (Npos (xO xH))))))))))))) POSTCONDITION *)
 forward_if.
 - (* then clause *)
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Tsh (Tstruct _tree noattr) (@pair val val p1 p2) r) (treerep t2 q)) (treerep t2 p2)) (treerep t1 p)) (treerep t1 p1)) (@data_at CompSpecs Tsh (Tstruct _tree noattr) (@pair val val p q) (Vptr b i))) (@exp mpred Nveric val (fun a : val => @andp mpred Nveric (@prop mpred Nveric (@eq val r a)) (@sepcon mpred Nveric Sveric (treerep (NODE t1 t2) (Vptr b i)) (treerep (NODE t1 t2) a)))) *)
   forward. simpl.
(* Goal: @derives mpred Nveric (@emp mpred Nveric Sveric) (@exp mpred Nveric val (fun a0 : val => @andp mpred Nveric (@prop mpred Nveric (@eq val (Vint (Int.repr (Z.add (Z.add i i) (Zpos xH)))) a0)) (@sepcon mpred Nveric Sveric (@andp mpred Nveric (@prop mpred Nveric (@eq val (Vint (Int.repr (Z.add (Z.add i i) (Zpos xH)))) (Vint (Int.repr (Z.add (Z.add i i) (Zpos xH)))))) (@emp mpred Nveric Sveric)) (@andp mpred Nveric (@prop mpred Nveric (@eq val a0 (Vint (Int.repr (Z.add (Z.add i i) (Zpos xH)))))) (@emp mpred Nveric Sveric))))) *)
   Exists (Vint (Int.repr(i+i+1))).
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Tsh (Tstruct _tree noattr) (@pair val val p1 p2) r) (treerep t2 q)) (treerep t2 p2)) (treerep t1 p)) (treerep t1 p1)) (@data_at CompSpecs Tsh (Tstruct _tree noattr) (@pair val val p q) (Vptr b i))) (@andp mpred Nveric (@prop mpred Nveric (@eq val r r)) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Tsh (Tstruct _tree noattr) (@pair val val p q) (Vptr b i)) (treerep t1 p)) (treerep t2 q)) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Tsh (Tstruct _tree noattr) (@pair val val p1 p2) r) (treerep t1 p1)) (treerep t2 p2)))) *)
   entailer!.
 - (* else clause *)
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _t'6 (Vint (Int.repr (Zpos xH)))) (@cons localdef (temp _t (Vint (Int.repr (Z.add (Z.add i i) (Zpos xH))))) (@nil localdef))) (SEPx (@cons mpred (@emp mpred Nveric Sveric) (@nil mpred))))) (Ssequence (Ssequence (Scall (@Some ident _t'1) (Evar _int_or_ptr_to_ptr (Tfunction (Tcons (Tpointer tvoid (mk_attr false (@Some N (Npos (xO xH))))) Tnil) (tptr tvoid) cc_default)) (@cons expr (Etempvar _t (Tpointer tvoid (mk_attr false (@Some N (Npos (xO xH)))))) (@nil expr))) (Sset _s (Ecast (Etempvar _t'1 (tptr tvoid)) (tptr (Tstruct _tree noattr))))) MORE_COMMANDS) POSTCONDITION *)
  inv H0.
* (* NODE *) 
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _t p) (@nil localdef)) (SEPx (@cons mpred (treerep (NODE t1 t2) p) (@nil mpred))))) (Ssequence (Scall (@Some ident _t'6) (Evar _test_int_or_ptr (Tfunction (Tcons (Tpointer tvoid (mk_attr false (@Some N (Npos (xO xH))))) Tnil) tint cc_default)) (@cons expr (Etempvar _t (Tpointer tvoid (mk_attr false (@Some N (Npos (xO xH)))))) (@nil expr))) MORE_COMMANDS) POSTCONDITION *)
  unfold treerep; fold treerep.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _t p) (@nil localdef)) (SEPx (@cons mpred (@exp mpred Nveric val (fun p1 : val => @exp mpred Nveric val (fun p2 : val => @sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Tsh (Tstruct _tree noattr) (@pair val val p1 p2) p) (treerep t1 p1)) (treerep t2 p2)))) (@nil mpred))))) (Ssequence (Scall (@Some ident _t'6) (Evar _test_int_or_ptr (Tfunction (Tcons (Tpointer tvoid (mk_attr false (@Some N (Npos (xO xH))))) Tnil) tint cc_default)) (@cons expr (Etempvar _t (Tpointer tvoid (mk_attr false (@Some N (Npos (xO xH)))))) (@nil expr))) MORE_COMMANDS) POSTCONDITION *)
  rename p into t.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _t t) (@nil localdef)) (SEPx (@cons mpred (@exp mpred Nveric val (fun p1 : val => @exp mpred Nveric val (fun p2 : val => @sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Tsh (Tstruct _tree noattr) (@pair val val p1 p2) t) (treerep t1 p1)) (treerep t2 p2)))) (@nil mpred))))) (Ssequence (Scall (@Some ident _t'6) (Evar _test_int_or_ptr (Tfunction (Tcons (Tpointer tvoid (mk_attr false (@Some N (Npos (xO xH))))) Tnil) tint cc_default)) (@cons expr (Etempvar _t (Tpointer tvoid (mk_attr false (@Some N (Npos (xO xH)))))) (@nil expr))) MORE_COMMANDS) POSTCONDITION *)
  Intros p q.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _t t) (@nil localdef)) (SEPx (@cons mpred (@data_at CompSpecs Tsh (Tstruct _tree noattr) (@pair val val p q) t) (@cons mpred (treerep t1 p) (@cons mpred (treerep t2 q) (@nil mpred))))))) (Ssequence (Scall (@Some ident _t'6) (Evar _test_int_or_ptr (Tfunction (Tcons (Tpointer tvoid (mk_attr false (@Some N (Npos (xO xH))))) Tnil) tint cc_default)) (@cons expr (Etempvar _t (Tpointer tvoid (mk_attr false (@Some N (Npos (xO xH)))))) (@nil expr))) MORE_COMMANDS) POSTCONDITION *)
  forward_call t.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Tsh (Tstruct _tree noattr) (@pair val val p1 p2) r) (treerep t2 q)) (treerep t2 p2)) (treerep t1 p)) (treerep t1 p1)) (@data_at CompSpecs Tsh (Tstruct _tree noattr) (@pair val val p q) (Vptr b i))) (@andp mpred Nveric (@prop mpred Nveric (@eq val r r)) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Tsh (Tstruct _tree noattr) (@pair val val p q) (Vptr b i)) (treerep t1 p)) (treerep t2 q)) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Tsh (Tstruct _tree noattr) (@pair val val p1 p2) r) (treerep t1 p1)) (treerep t2 p2)))) *)
  assert_PROP (isptr t) by entailer!.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _t'6 (Vint (Int.repr match t with | Vundef => Z0 | Vint i => Zpos xH | Vlong i => Z0 | Vfloat f => Z0 | Vsingle f => Z0 | Vptr b i => Z0 end))) (@cons localdef (temp _t t) (@nil localdef))) (SEPx (@cons mpred (@data_at CompSpecs Tsh (Tstruct _tree noattr) (@pair val val p q) t) (@cons mpred (treerep t1 p) (@cons mpred (treerep t2 q) (@nil mpred))))))) (Sifthenelse (Etempvar _t'6 tint) (Sreturn (@Some expr (Etempvar _t (Tpointer tvoid (mk_attr false (@Some N (Npos (xO xH)))))))) (Ssequence (Ssequence (Scall (@Some ident _t'1) (Evar _int_or_ptr_to_ptr (Tfunction (Tcons (Tpointer tvoid (mk_attr false (@Some N (Npos (xO xH))))) Tnil) (tptr tvoid) cc_default)) (@cons expr (Etempvar _t (Tpointer tvoid (mk_attr false (@Some N (Npos (xO xH)))))) (@nil expr))) (Sset _s (Ecast (Etempvar _t'1 (tptr tvoid)) (tptr (Tstruct _tree noattr))))) (Ssequence (Ssequence (Ssequence (Sset _t'8 (Efield (Ederef (Etempvar _s (tptr (Tstruct _tree noattr))) (Tstruct _tree noattr)) _left (Tpointer tvoid (mk_attr false (@Some N (Npos (xO xH))))))) (Scall (@Some ident _t'2) (Evar _copytree (Tfunction (Tcons (Tpointer tvoid (mk_attr false (@Some N (Npos (xO xH))))) Tnil) (Tpointer tvoid (mk_attr false (@Some N (Npos (xO xH))))) cc_default)) (@cons expr (Etempvar _t'8 (Tpointer tvoid (mk_attr false (@Some N (Npos (xO xH)))))) (@nil expr)))) (Sset _p (Etempvar _t'2 (Tpointer tvoid (mk_attr false (@Some N (Npos (xO xH)))))))) (Ssequence (Ssequence (Ssequence (Sset _t'7 (Efield (Ederef (Etempvar _s (tptr (Tstruct _tree noattr))) (Tstruct _tree noattr)) _right (Tpointer tvoid (mk_attr false (@Some N (Npos (xO xH))))))) (Scall (@Some ident _t'3) (Evar _copytree (Tfunction (Tcons (Tpointer tvoid (mk_attr false (@Some N (Npos (xO xH))))) Tnil) (Tpointer tvoid (mk_attr false (@Some N (Npos (xO xH))))) cc_default)) (@cons expr (Etempvar _t'7 (Tpointer tvoid (mk_attr false (@Some N (Npos (xO xH)))))) (@nil expr)))) (Sset _q (Etempvar _t'3 (Tpointer tvoid (mk_attr false (@Some N (Npos (xO xH)))))))) (Ssequence (Ssequence (Scall (@Some ident _t'4) (Evar _makenode (Tfunction (Tcons (Tpointer tvoid (mk_attr false (@Some N (Npos (xO xH))))) (Tcons (Tpointer tvoid (mk_attr false (@Some N (Npos (xO xH))))) Tnil)) (tptr (Tstruct _tree noattr)) cc_default)) (@cons expr (Etempvar _p (Tpointer tvoid (mk_attr false (@Some N (Npos (xO xH)))))) (@cons expr (Etempvar _q (Tpointer tvoid (mk_attr false (@Some N (Npos (xO xH)))))) (@nil expr)))) (Scall (@Some ident _t'5) (Evar _ptr_to_int_or_ptr (Tfunction (Tcons (tptr tvoid) Tnil) (Tpointer tvoid (mk_attr false (@Some N (Npos (xO xH))))) cc_default)) (@cons expr (Etempvar _t'4 (tptr (Tstruct _tree noattr))) (@nil expr)))) (Sreturn (@Some expr (Etempvar _t'5 (Tpointer tvoid (mk_attr false (@Some N (Npos (xO xH))))))))))))) POSTCONDITION *)
  destruct t; try contradiction. clear H0.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _t'6 (Vint (Int.repr Z0))) (@cons localdef (temp _t (Vptr b i)) (@nil localdef))) (SEPx (@cons mpred (@data_at CompSpecs Tsh (Tstruct _tree noattr) (@pair val val p q) (Vptr b i)) (@cons mpred (treerep t1 p) (@cons mpred (treerep t2 q) (@nil mpred))))))) (Sifthenelse (Etempvar _t'6 tint) (Sreturn (@Some expr (Etempvar _t (Tpointer tvoid (mk_attr false (@Some N (Npos (xO xH)))))))) (Ssequence (Ssequence (Scall (@Some ident _t'1) (Evar _int_or_ptr_to_ptr (Tfunction (Tcons (Tpointer tvoid (mk_attr false (@Some N (Npos (xO xH))))) Tnil) (tptr tvoid) cc_default)) (@cons expr (Etempvar _t (Tpointer tvoid (mk_attr false (@Some N (Npos (xO xH)))))) (@nil expr))) (Sset _s (Ecast (Etempvar _t'1 (tptr tvoid)) (tptr (Tstruct _tree noattr))))) (Ssequence (Ssequence (Ssequence (Sset _t'8 (Efield (Ederef (Etempvar _s (tptr (Tstruct _tree noattr))) (Tstruct _tree noattr)) _left (Tpointer tvoid (mk_attr false (@Some N (Npos (xO xH))))))) (Scall (@Some ident _t'2) (Evar _copytree (Tfunction (Tcons (Tpointer tvoid (mk_attr false (@Some N (Npos (xO xH))))) Tnil) (Tpointer tvoid (mk_attr false (@Some N (Npos (xO xH))))) cc_default)) (@cons expr (Etempvar _t'8 (Tpointer tvoid (mk_attr false (@Some N (Npos (xO xH)))))) (@nil expr)))) (Sset _p (Etempvar _t'2 (Tpointer tvoid (mk_attr false (@Some N (Npos (xO xH)))))))) (Ssequence (Ssequence (Ssequence (Sset _t'7 (Efield (Ederef (Etempvar _s (tptr (Tstruct _tree noattr))) (Tstruct _tree noattr)) _right (Tpointer tvoid (mk_attr false (@Some N (Npos (xO xH))))))) (Scall (@Some ident _t'3) (Evar _copytree (Tfunction (Tcons (Tpointer tvoid (mk_attr false (@Some N (Npos (xO xH))))) Tnil) (Tpointer tvoid (mk_attr false (@Some N (Npos (xO xH))))) cc_default)) (@cons expr (Etempvar _t'7 (Tpointer tvoid (mk_attr false (@Some N (Npos (xO xH)))))) (@nil expr)))) (Sset _q (Etempvar _t'3 (Tpointer tvoid (mk_attr false (@Some N (Npos (xO xH)))))))) (Ssequence (Ssequence (Scall (@Some ident _t'4) (Evar _makenode (Tfunction (Tcons (Tpointer tvoid (mk_attr false (@Some N (Npos (xO xH))))) (Tcons (Tpointer tvoid (mk_attr false (@Some N (Npos (xO xH))))) Tnil)) (tptr (Tstruct _tree noattr)) cc_default)) (@cons expr (Etempvar _p (Tpointer tvoid (mk_attr false (@Some N (Npos (xO xH)))))) (@cons expr (Etempvar _q (Tpointer tvoid (mk_attr false (@Some N (Npos (xO xH)))))) (@nil expr)))) (Scall (@Some ident _t'5) (Evar _ptr_to_int_or_ptr (Tfunction (Tcons (tptr tvoid) Tnil) (Tpointer tvoid (mk_attr false (@Some N (Npos (xO xH))))) cc_default)) (@cons expr (Etempvar _t'4 (tptr (Tstruct _tree noattr))) (@nil expr)))) (Sreturn (@Some expr (Etempvar _t'5 (Tpointer tvoid (mk_attr false (@Some N (Npos (xO xH))))))))))))) POSTCONDITION *)
  forward_if.
  - (* then clause *)
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _t'6 (Vint (Int.repr Z0))) (@cons localdef (temp _t (Vptr b i)) (@nil localdef))) (SEPx (@cons mpred (@data_at CompSpecs Tsh (Tstruct _tree noattr) (@pair val val p q) (Vptr b i)) (@cons mpred (treerep t1 p) (@cons mpred (treerep t2 q) (@nil mpred))))))) (Sreturn (@Some expr (Etempvar _t (Tpointer tvoid (mk_attr false (@Some N (Npos (xO xH)))))))) POSTCONDITION *)
    contradiction.
  - (* else clause *)
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _t'6 (Vint (Int.repr Z0))) (@cons localdef (temp _t (Vptr b i)) (@nil localdef))) (SEPx (@cons mpred (@data_at CompSpecs Tsh (Tstruct _tree noattr) (@pair val val p q) (Vptr b i)) (@cons mpred (treerep t1 p) (@cons mpred (treerep t2 q) (@nil mpred))))))) (Ssequence (Ssequence (Scall (@Some ident _t'1) (Evar _int_or_ptr_to_ptr (Tfunction (Tcons (Tpointer tvoid (mk_attr false (@Some N (Npos (xO xH))))) Tnil) (tptr tvoid) cc_default)) (@cons expr (Etempvar _t (Tpointer tvoid (mk_attr false (@Some N (Npos (xO xH)))))) (@nil expr))) (Sset _s (Ecast (Etempvar _t'1 (tptr tvoid)) (tptr (Tstruct _tree noattr))))) MORE_COMMANDS) POSTCONDITION *)
   clear H0. simpl in H.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _t'6 (Vint (Int.repr Z0))) (@cons localdef (temp _t (Vptr b i)) (@nil localdef))) (SEPx (@cons mpred (@data_at CompSpecs Tsh (Tstruct _tree noattr) (@pair val val p q) (Vptr b i)) (@cons mpred (treerep t1 p) (@cons mpred (treerep t2 q) (@nil mpred))))))) (Ssequence (Ssequence (Scall (@Some ident _t'1) (Evar _int_or_ptr_to_ptr (Tfunction (Tcons (Tpointer tvoid (mk_attr false (@Some N (Npos (xO xH))))) Tnil) (tptr tvoid) cc_default)) (@cons expr (Etempvar _t (Tpointer tvoid (mk_attr false (@Some N (Npos (xO xH)))))) (@nil expr))) (Sset _s (Ecast (Etempvar _t'1 (tptr tvoid)) (tptr (Tstruct _tree noattr))))) MORE_COMMANDS) POSTCONDITION *)
   forward_call (Vptr b i).
(* Goal: isptr (Vptr b i) *)
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _s (Vptr b i)) (@cons localdef (temp _t'6 (Vint (Int.repr Z0))) (@cons localdef (temp _t (Vptr b i)) (@nil localdef)))) (SEPx (@cons mpred (@data_at CompSpecs Tsh (Tstruct _tree noattr) (@pair val val p q) (Vptr b i)) (@cons mpred (treerep t1 p) (@cons mpred (treerep t2 q) (@nil mpred))))))) (Ssequence (Ssequence (Ssequence (Sset _t'8 (Efield (Ederef (Etempvar _s (tptr (Tstruct _tree noattr))) (Tstruct _tree noattr)) _left (Tpointer tvoid (mk_attr false (@Some N (Npos (xO xH))))))) (Scall (@Some ident _t'2) (Evar _copytree (Tfunction (Tcons (Tpointer tvoid (mk_attr false (@Some N (Npos (xO xH))))) Tnil) (Tpointer tvoid (mk_attr false (@Some N (Npos (xO xH))))) cc_default)) (@cons expr (Etempvar _t'8 (Tpointer tvoid (mk_attr false (@Some N (Npos (xO xH)))))) (@nil expr)))) (Sset _p (Etempvar _t'2 (Tpointer tvoid (mk_attr false (@Some N (Npos (xO xH)))))))) MORE_COMMANDS) POSTCONDITION *)
   apply I.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _t'5 r) (@cons localdef (temp _t'4 r) (@cons localdef (temp _q p2) (@cons localdef (temp _p p1) (@nil localdef))))) (SEPx (@cons mpred (@data_at CompSpecs Tsh (Tstruct _tree noattr) (@pair val val p1 p2) r) (@cons mpred (treerep t2 q) (@cons mpred (treerep t2 p2) (@cons mpred (treerep t1 p) (@cons mpred (treerep t1 p1) (@cons mpred (@data_at CompSpecs Tsh (Tstruct _tree noattr) (@pair val val p q) (Vptr b i)) (@nil mpred)))))))))) (Sreturn (@Some expr (Etempvar _t'5 (Tpointer tvoid (mk_attr false (@Some N (Npos (xO xH)))))))) POSTCONDITION *)
   forward.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Tsh (Tstruct _tree noattr) (@pair val val p1 p2) r) (treerep t2 q)) (treerep t2 p2)) (treerep t1 p)) (treerep t1 p1)) (@data_at CompSpecs Tsh (Tstruct _tree noattr) (@pair val val p q) (Vptr b i))) (@andp mpred Nveric (@prop mpred Nveric (@eq val r r)) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Tsh (Tstruct _tree noattr) (@pair val val p q) (Vptr b i)) (treerep t1 p)) (treerep t2 q)) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Tsh (Tstruct _tree noattr) (@pair val val p1 p2) r) (treerep t1 p1)) (treerep t2 p2)))) *)
     entailer!.
(* Goal: isptr (Vptr b i) *)
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _s (Vptr b i)) (@cons localdef (temp _t'6 (Vint (Int.repr Z0))) (@cons localdef (temp _t (Vptr b i)) (@nil localdef)))) (SEPx (@cons mpred (@data_at CompSpecs Tsh (Tstruct _tree noattr) (@pair val val p q) (Vptr b i)) (@cons mpred (treerep t1 p) (@cons mpred (treerep t2 q) (@nil mpred))))))) (Ssequence (Ssequence (Ssequence (Sset _t'8 (Efield (Ederef (Etempvar _s (tptr (Tstruct _tree noattr))) (Tstruct _tree noattr)) _left (Tpointer tvoid (mk_attr false (@Some N (Npos (xO xH))))))) (Scall (@Some ident _t'2) (Evar _copytree (Tfunction (Tcons (Tpointer tvoid (mk_attr false (@Some N (Npos (xO xH))))) Tnil) (Tpointer tvoid (mk_attr false (@Some N (Npos (xO xH))))) cc_default)) (@cons expr (Etempvar _t'8 (Tpointer tvoid (mk_attr false (@Some N (Npos (xO xH)))))) (@nil expr)))) (Sset _p (Etempvar _t'2 (Tpointer tvoid (mk_attr false (@Some N (Npos (xO xH)))))))) MORE_COMMANDS) POSTCONDITION *)
     destruct p; try contradiction; apply I.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _t'8 p) (@cons localdef (temp _s (Vptr b i)) (@cons localdef (temp _t'6 (Vint (Int.repr Z0))) (@cons localdef (temp _t (Vptr b i)) (@nil localdef))))) (SEPx (@cons mpred (@data_at CompSpecs Tsh (Tstruct _tree noattr) (@pair val val p q) (Vptr b i)) (@cons mpred (treerep t1 p) (@cons mpred (treerep t2 q) (@nil mpred))))))) (Ssequence (Scall (@Some ident _t'2) (Evar _copytree (Tfunction (Tcons (Tpointer tvoid (mk_attr false (@Some N (Npos (xO xH))))) Tnil) (Tpointer tvoid (mk_attr false (@Some N (Npos (xO xH))))) cc_default)) (@cons expr (Etempvar _t'8 (Tpointer tvoid (mk_attr false (@Some N (Npos (xO xH)))))) (@nil expr))) MORE_COMMANDS) POSTCONDITION *)
   forward_call (t1,p).
(* Goal: semax CompSpecs Espec Delta (@exp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) val (fun vret : val => PROPx (@nil Prop) (LOCALx (@cons localdef (temp _t'2 vret) (@cons localdef (temp _t'8 p) (@cons localdef (temp _s (Vptr b i)) (@cons localdef (temp _t'6 (Vint (Int.repr Z0))) (@cons localdef (temp _t (Vptr b i)) (@nil localdef)))))) (SEPx (@cons mpred (treerep t1 p) (@cons mpred (treerep t1 vret) (@cons mpred (@data_at CompSpecs Tsh (Tstruct _tree noattr) (@pair val val p q) (Vptr b i)) (@cons mpred (treerep t2 q) (@nil mpred))))))))) (Ssequence (Sset _p (Etempvar _t'2 (Tpointer tvoid (mk_attr false (@Some N (Npos (xO xH))))))) MORE_COMMANDS) POSTCONDITION *)
   Intros p1.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _q p2) (@cons localdef (temp _t'3 p2) (@cons localdef (temp _t'7 q) (@cons localdef (temp _p p1) (@cons localdef (temp _t'2 p1) (@cons localdef (temp _s (Vptr b i)) (@nil localdef))))))) (SEPx (@cons mpred (treerep t2 q) (@cons mpred (treerep t2 p2) (@cons mpred (treerep t1 p) (@cons mpred (treerep t1 p1) (@cons mpred (@data_at CompSpecs Tsh (Tstruct _tree noattr) (@pair val val p q) (Vptr b i)) (@nil mpred))))))))) (Ssequence (Ssequence (Scall (@Some ident _t'4) (Evar _makenode (Tfunction (Tcons (Tpointer tvoid (mk_attr false (@Some N (Npos (xO xH))))) (Tcons (Tpointer tvoid (mk_attr false (@Some N (Npos (xO xH))))) Tnil)) (tptr (Tstruct _tree noattr)) cc_default)) (@cons expr (Etempvar _p (Tpointer tvoid (mk_attr false (@Some N (Npos (xO xH)))))) (@cons expr (Etempvar _q (Tpointer tvoid (mk_attr false (@Some N (Npos (xO xH)))))) (@nil expr)))) (Scall (@Some ident _t'5) (Evar _ptr_to_int_or_ptr (Tfunction (Tcons (tptr tvoid) Tnil) (Tpointer tvoid (mk_attr false (@Some N (Npos (xO xH))))) cc_default)) (@cons expr (Etempvar _t'4 (tptr (Tstruct _tree noattr))) (@nil expr)))) MORE_COMMANDS) POSTCONDITION *)
   deadvars.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _t'5 r) (@cons localdef (temp _t'4 r) (@cons localdef (temp _q p2) (@cons localdef (temp _p p1) (@nil localdef))))) (SEPx (@cons mpred (@data_at CompSpecs Tsh (Tstruct _tree noattr) (@pair val val p1 p2) r) (@cons mpred (treerep t2 q) (@cons mpred (treerep t2 p2) (@cons mpred (treerep t1 p) (@cons mpred (treerep t1 p1) (@cons mpred (@data_at CompSpecs Tsh (Tstruct _tree noattr) (@pair val val p q) (Vptr b i)) (@nil mpred)))))))))) (Sreturn (@Some expr (Etempvar _t'5 (Tpointer tvoid (mk_attr false (@Some N (Npos (xO xH)))))))) POSTCONDITION *)
   forward.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _t'5 r) (@cons localdef (temp _t'4 r) (@cons localdef (temp _q p2) (@cons localdef (temp _p p1) (@nil localdef))))) (SEPx (@cons mpred (@data_at CompSpecs Tsh (Tstruct _tree noattr) (@pair val val p1 p2) r) (@cons mpred (treerep t2 q) (@cons mpred (treerep t2 p2) (@cons mpred (treerep t1 p) (@cons mpred (treerep t1 p1) (@cons mpred (@data_at CompSpecs Tsh (Tstruct _tree noattr) (@pair val val p q) (Vptr b i)) (@nil mpred)))))))))) (Sreturn (@Some expr (Etempvar _t'5 (Tpointer tvoid (mk_attr false (@Some N (Npos (xO xH)))))))) POSTCONDITION *)
   forward.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Tsh (Tstruct _tree noattr) (@pair val val p1 p2) r) (treerep t2 q)) (treerep t2 p2)) (treerep t1 p)) (treerep t1 p1)) (@data_at CompSpecs Tsh (Tstruct _tree noattr) (@pair val val p q) (Vptr b i))) (@andp mpred Nveric (@prop mpred Nveric (@eq val r r)) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Tsh (Tstruct _tree noattr) (@pair val val p q) (Vptr b i)) (treerep t1 p)) (treerep t2 q)) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Tsh (Tstruct _tree noattr) (@pair val val p1 p2) r) (treerep t1 p1)) (treerep t2 p2)))) *)
    entailer!.
(* Goal: isptr (Vptr b i) *)
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _s (Vptr b i)) (@cons localdef (temp _t'6 (Vint (Int.repr Z0))) (@cons localdef (temp _t (Vptr b i)) (@nil localdef)))) (SEPx (@cons mpred (@data_at CompSpecs Tsh (Tstruct _tree noattr) (@pair val val p q) (Vptr b i)) (@cons mpred (treerep t1 p) (@cons mpred (treerep t2 q) (@nil mpred))))))) (Ssequence (Ssequence (Ssequence (Sset _t'8 (Efield (Ederef (Etempvar _s (tptr (Tstruct _tree noattr))) (Tstruct _tree noattr)) _left (Tpointer tvoid (mk_attr false (@Some N (Npos (xO xH))))))) (Scall (@Some ident _t'2) (Evar _copytree (Tfunction (Tcons (Tpointer tvoid (mk_attr false (@Some N (Npos (xO xH))))) Tnil) (Tpointer tvoid (mk_attr false (@Some N (Npos (xO xH))))) cc_default)) (@cons expr (Etempvar _t'8 (Tpointer tvoid (mk_attr false (@Some N (Npos (xO xH)))))) (@nil expr)))) (Sset _p (Etempvar _t'2 (Tpointer tvoid (mk_attr false (@Some N (Npos (xO xH)))))))) MORE_COMMANDS) POSTCONDITION *)
     destruct q; try contradiction; apply I.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _t'7 q) (@cons localdef (temp _p p1) (@cons localdef (temp _t'2 p1) (@cons localdef (temp _s (Vptr b i)) (@nil localdef))))) (SEPx (@cons mpred (treerep t1 p) (@cons mpred (treerep t1 p1) (@cons mpred (@data_at CompSpecs Tsh (Tstruct _tree noattr) (@pair val val p q) (Vptr b i)) (@cons mpred (treerep t2 q) (@nil mpred)))))))) (Ssequence (Scall (@Some ident _t'3) (Evar _copytree (Tfunction (Tcons (Tpointer tvoid (mk_attr false (@Some N (Npos (xO xH))))) Tnil) (Tpointer tvoid (mk_attr false (@Some N (Npos (xO xH))))) cc_default)) (@cons expr (Etempvar _t'7 (Tpointer tvoid (mk_attr false (@Some N (Npos (xO xH)))))) (@nil expr))) MORE_COMMANDS) POSTCONDITION *)
   forward_call (t2,q).
(* Goal: semax CompSpecs Espec Delta (@exp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) val (fun vret : val => PROPx (@nil Prop) (LOCALx (@cons localdef (temp _t'3 vret) (@cons localdef (temp _t'7 q) (@cons localdef (temp _p p1) (@cons localdef (temp _t'2 p1) (@cons localdef (temp _s (Vptr b i)) (@nil localdef)))))) (SEPx (@cons mpred (treerep t2 q) (@cons mpred (treerep t2 vret) (@cons mpred (treerep t1 p) (@cons mpred (treerep t1 p1) (@cons mpred (@data_at CompSpecs Tsh (Tstruct _tree noattr) (@pair val val p q) (Vptr b i)) (@nil mpred)))))))))) (Ssequence (Sset _q (Etempvar _t'3 (Tpointer tvoid (mk_attr false (@Some N (Npos (xO xH))))))) MORE_COMMANDS) POSTCONDITION *)
   Intros p2.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _t'5 r) (@cons localdef (temp _t'4 r) (@cons localdef (temp _q p2) (@cons localdef (temp _p p1) (@nil localdef))))) (SEPx (@cons mpred (@data_at CompSpecs Tsh (Tstruct _tree noattr) (@pair val val p1 p2) r) (@cons mpred (treerep t2 q) (@cons mpred (treerep t2 p2) (@cons mpred (treerep t1 p) (@cons mpred (treerep t1 p1) (@cons mpred (@data_at CompSpecs Tsh (Tstruct _tree noattr) (@pair val val p q) (Vptr b i)) (@nil mpred)))))))))) (Sreturn (@Some expr (Etempvar _t'5 (Tpointer tvoid (mk_attr false (@Some N (Npos (xO xH)))))))) POSTCONDITION *)
   forward.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _q p2) (@cons localdef (temp _t'3 p2) (@cons localdef (temp _t'7 q) (@cons localdef (temp _p p1) (@cons localdef (temp _t'2 p1) (@cons localdef (temp _s (Vptr b i)) (@nil localdef))))))) (SEPx (@cons mpred (treerep t2 q) (@cons mpred (treerep t2 p2) (@cons mpred (treerep t1 p) (@cons mpred (treerep t1 p1) (@cons mpred (@data_at CompSpecs Tsh (Tstruct _tree noattr) (@pair val val p q) (Vptr b i)) (@nil mpred))))))))) (Ssequence (Ssequence (Scall (@Some ident _t'4) (Evar _makenode (Tfunction (Tcons (Tpointer tvoid (mk_attr false (@Some N (Npos (xO xH))))) (Tcons (Tpointer tvoid (mk_attr false (@Some N (Npos (xO xH))))) Tnil)) (tptr (Tstruct _tree noattr)) cc_default)) (@cons expr (Etempvar _p (Tpointer tvoid (mk_attr false (@Some N (Npos (xO xH)))))) (@cons expr (Etempvar _q (Tpointer tvoid (mk_attr false (@Some N (Npos (xO xH)))))) (@nil expr)))) (Scall (@Some ident _t'5) (Evar _ptr_to_int_or_ptr (Tfunction (Tcons (tptr tvoid) Tnil) (Tpointer tvoid (mk_attr false (@Some N (Npos (xO xH))))) cc_default)) (@cons expr (Etempvar _t'4 (tptr (Tstruct _tree noattr))) (@nil expr)))) MORE_COMMANDS) POSTCONDITION *)
   deadvars.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _q p2) (@cons localdef (temp _p p1) (@nil localdef))) (SEPx (@cons mpred (treerep t2 q) (@cons mpred (treerep t2 p2) (@cons mpred (treerep t1 p) (@cons mpred (treerep t1 p1) (@cons mpred (@data_at CompSpecs Tsh (Tstruct _tree noattr) (@pair val val p q) (Vptr b i)) (@nil mpred))))))))) (Ssequence (Ssequence (Scall (@Some ident _t'4) (Evar _makenode (Tfunction (Tcons (Tpointer tvoid (mk_attr false (@Some N (Npos (xO xH))))) (Tcons (Tpointer tvoid (mk_attr false (@Some N (Npos (xO xH))))) Tnil)) (tptr (Tstruct _tree noattr)) cc_default)) (@cons expr (Etempvar _p (Tpointer tvoid (mk_attr false (@Some N (Npos (xO xH)))))) (@cons expr (Etempvar _q (Tpointer tvoid (mk_attr false (@Some N (Npos (xO xH)))))) (@nil expr)))) (Scall (@Some ident _t'5) (Evar _ptr_to_int_or_ptr (Tfunction (Tcons (tptr tvoid) Tnil) (Tpointer tvoid (mk_attr false (@Some N (Npos (xO xH))))) cc_default)) (@cons expr (Etempvar _t'4 (tptr (Tstruct _tree noattr))) (@nil expr)))) MORE_COMMANDS) POSTCONDITION *)
   forward_call (p1,p2).
(* Goal: semax CompSpecs Espec Delta (@exp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) val (fun vret : val => PROPx (@nil Prop) (LOCALx (@cons localdef (temp _t'4 vret) (@cons localdef (temp _q p2) (@cons localdef (temp _p p1) (@nil localdef)))) (SEPx (@cons mpred (@data_at CompSpecs Tsh (Tstruct _tree noattr) (@pair val val p1 p2) vret) (@cons mpred (treerep t2 q) (@cons mpred (treerep t2 p2) (@cons mpred (treerep t1 p) (@cons mpred (treerep t1 p1) (@cons mpred (@data_at CompSpecs Tsh (Tstruct _tree noattr) (@pair val val p q) (Vptr b i)) (@nil mpred))))))))))) (Ssequence (Scall (@Some ident _t'5) (Evar _ptr_to_int_or_ptr (Tfunction (Tcons (tptr tvoid) Tnil) (Tpointer tvoid (mk_attr false (@Some N (Npos (xO xH))))) cc_default)) (@cons expr (Etempvar _t'4 (tptr (Tstruct _tree noattr))) (@nil expr))) MORE_COMMANDS) POSTCONDITION *)
  Intros r.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _t'4 r) (@cons localdef (temp _q p2) (@cons localdef (temp _p p1) (@nil localdef)))) (SEPx (@cons mpred (@data_at CompSpecs Tsh (Tstruct _tree noattr) (@pair val val p1 p2) r) (@cons mpred (treerep t2 q) (@cons mpred (treerep t2 p2) (@cons mpred (treerep t1 p) (@cons mpred (treerep t1 p1) (@cons mpred (@data_at CompSpecs Tsh (Tstruct _tree noattr) (@pair val val p q) (Vptr b i)) (@nil mpred)))))))))) (Ssequence (Scall (@Some ident _t'5) (Evar _ptr_to_int_or_ptr (Tfunction (Tcons (tptr tvoid) Tnil) (Tpointer tvoid (mk_attr false (@Some N (Npos (xO xH))))) cc_default)) (@cons expr (Etempvar _t'4 (tptr (Tstruct _tree noattr))) (@nil expr))) MORE_COMMANDS) POSTCONDITION *)
  assert_PROP (valid_int_or_ptr r). {
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Tsh (Tstruct _tree noattr) (@pair val val p1 p2) r) (treerep t2 q)) (treerep t2 p2)) (treerep t1 p)) (treerep t1 p1)) (@data_at CompSpecs Tsh (Tstruct _tree noattr) (@pair val val p q) (Vptr b i))) (@andp mpred Nveric (@prop mpred Nveric (@eq val r r)) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Tsh (Tstruct _tree noattr) (@pair val val p q) (Vptr b i)) (treerep t1 p)) (treerep t2 q)) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Tsh (Tstruct _tree noattr) (@pair val val p1 p2) r) (treerep t1 p1)) (treerep t2 p2)))) *)
    entailer!.
(* Goal: valid_int_or_ptr r *)
    apply field_compatible_valid_int_or_ptr; auto.
  }
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _t'4 r) (@cons localdef (temp _q p2) (@cons localdef (temp _p p1) (@nil localdef)))) (SEPx (@cons mpred (@data_at CompSpecs Tsh (Tstruct _tree noattr) (@pair val val p1 p2) r) (@cons mpred (treerep t2 q) (@cons mpred (treerep t2 p2) (@cons mpred (treerep t1 p) (@cons mpred (treerep t1 p1) (@cons mpred (@data_at CompSpecs Tsh (Tstruct _tree noattr) (@pair val val p q) (Vptr b i)) (@nil mpred)))))))))) (Ssequence (Scall (@Some ident _t'5) (Evar _ptr_to_int_or_ptr (Tfunction (Tcons (tptr tvoid) Tnil) (Tpointer tvoid (mk_attr false (@Some N (Npos (xO xH))))) cc_default)) (@cons expr (Etempvar _t'4 (tptr (Tstruct _tree noattr))) (@nil expr))) MORE_COMMANDS) POSTCONDITION *)
  forward_call r.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Tsh (Tstruct _tree noattr) (@pair val val p1 p2) r) (treerep t2 q)) (treerep t2 p2)) (treerep t1 p)) (treerep t1 p1)) (@data_at CompSpecs Tsh (Tstruct _tree noattr) (@pair val val p q) (Vptr b i))) (@exp mpred Nveric val (fun a : val => @andp mpred Nveric (@prop mpred Nveric (@eq val r a)) (@sepcon mpred Nveric Sveric (treerep (NODE t1 t2) (Vptr b i)) (treerep (NODE t1 t2) a)))) *)
  forward. simpl.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Tsh (Tstruct _tree noattr) (@pair val val p1 p2) r) (treerep t2 q)) (treerep t2 p2)) (treerep t1 p)) (treerep t1 p1)) (@data_at CompSpecs Tsh (Tstruct _tree noattr) (@pair val val p q) (Vptr b i))) (@exp mpred Nveric val (fun a : val => @andp mpred Nveric (@prop mpred Nveric (@eq val r a)) (@sepcon mpred Nveric Sveric (@exp mpred Nveric val (fun p1 : val => @exp mpred Nveric val (fun p2 : val => @sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Tsh (Tstruct _tree noattr) (@pair val val p1 p2) (Vptr b i)) (treerep t1 p1)) (treerep t2 p2)))) (@exp mpred Nveric val (fun p1 : val => @exp mpred Nveric val (fun p2 : val => @sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Tsh (Tstruct _tree noattr) (@pair val val p1 p2) a) (treerep t1 p1)) (treerep t2 p2))))))) *)
  Exists r p q p1 p2.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Tsh (Tstruct _tree noattr) (@pair val val p1 p2) r) (treerep t2 q)) (treerep t2 p2)) (treerep t1 p)) (treerep t1 p1)) (@data_at CompSpecs Tsh (Tstruct _tree noattr) (@pair val val p q) (Vptr b i))) (@andp mpred Nveric (@prop mpred Nveric (@eq val r r)) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Tsh (Tstruct _tree noattr) (@pair val val p q) (Vptr b i)) (treerep t1 p)) (treerep t2 q)) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Tsh (Tstruct _tree noattr) (@pair val val p1 p2) r) (treerep t1 p1)) (treerep t2 p2)))) *)
  entailer!.
Qed.


