Require Import VST.floyd.proofauto.
Require Import VST.floyd.library.
Require Import VST.progs.list_dt.  Import LsegSpecial.
Require Import VST.progs.queue2.

Instance CompSpecs : compspecs. make_compspecs prog. Defined.
Definition Vprog : varspecs. mk_varspecs prog. Defined.

Definition t_struct_elem := Tstruct _elem noattr.
Definition t_struct_fifo := Tstruct _fifo noattr.

Instance QS: listspec _elem _next (fun sh => malloc_token Ews t_struct_elem).
Proof. eapply mk_listspec; reflexivity. Defined.

Lemma isnil: forall {T: Type} (s: list T), {s=nil}+{s<>nil}.
(* Goal: forall (al : list val) (q : val), @derives mpred Nveric (fifo al q) (@prop mpred Nveric (isptr q)) *)
Proof. intros. destruct s; [left|right]; auto. intro Hx; inv Hx. Qed.

Lemma field_at_list_cell:
  forall sh i v p,
  data_at sh t_struct_elem (i,v) p
  = list_cell QS sh i p *
  field_at sh t_struct_elem [StructField _next] v p.
Proof.
(* Goal: forall (al : list val) (q : val), @derives mpred Nveric (fifo al q) (@prop mpred Nveric (isptr q)) *)
intros.
(* Goal: @eq mpred (@data_at CompSpecs sh t_struct_elem (@pair (let (t, _) := @eq_rect Type ((fun it : prod ident type => (fun _ : type => @sigT Type (fun x : Type => x)) (field_type (@fst ident type it) (co_members (@get_co CompSpecs _elem)))) (@pair ident type _data tint)) (fun A0 : Type => A0) ((fun it : prod ident type => (fix type_func_rec (n : nat) (t : type) {struct n} : (fun _ : type => @sigT Type (fun x : Type => x)) t := match n with | O => match t as t0 return ((fun _ : type => @sigT Type (fun x : Type => x)) t0) with | Tvoid => (fun t0 : type => if type_is_by_value t0 then @existT Type (fun x : Type => x) val Vundef else @existT Type (fun x : Type => x) unit tt) Tvoid | Tint i s a => (fun t0 : type => if type_is_by_value t0 then @existT Type (fun x : Type => x) val Vundef else @existT Type (fun x : Type => x) unit tt) (Tint i s a) | Tlong s a => (fun t0 : type => if type_is_by_value t0 then @existT Type (fun x : Type => x) val Vundef else @existT Type (fun x : Type => x) unit tt) (Tlong s a) | Tfloat f a => (fun t0 : type => if type_is_by_value t0 then @existT Type (fun x : Type => x) val Vundef else @existT Type (fun x : Type => x) unit tt) (Tfloat f a) | Tpointer t0 a => (fun t1 : type => if type_is_by_value t1 then @existT Type (fun x : Type => x) val Vundef else @existT Type (fun x : Type => x) unit tt) (Tpointer t0 a) | Tarray t0 z a => (fun t1 : type => if type_is_by_value t1 then @existT Type (fun x : Type => x) val Vundef else @existT Type (fun x : Type => x) unit tt) (Tarray t0 z a) | Tfunction t0 t1 c => (fun t2 : type => if type_is_by_value t2 then @existT Type (fun x : Type => x) val Vundef else @existT Type (fun x : Type => x) unit tt) (Tfunction t0 t1 c) | Tstruct id a => match @PTree.get composite id (@cenv_cs CompSpecs) with | Some c => (fun t0 : type => if type_is_by_value t0 then @existT Type (fun x : Type => x) val Vundef else @existT Type (fun x : Type => x) unit tt) (Tstruct id a) | None => (fun (id0 : positive) (_ : attr) (TVs : @type_induction.FT_aux CompSpecs (fun _ : type => @sigT Type (fun x : Type => x)) id0) => @existT Type (fun x : Type => x) (@compact_prod_sigT_type Type (fun x : Type => x) (@type_induction.decay (prod ident type) (@sigT Type (fun x : Type => x)) (co_members (@get_co CompSpecs id0)) TVs)) (@compact_prod_sigT_value Type (fun x : Type => x) (@type_induction.decay (prod ident type) (@sigT Type (fun x : Type => x)) (co_members (@get_co CompSpecs id0)) TVs))) id a (@type_induction.ListTypeGen (prod ident type) (fun it0 : prod ident type => (fun _ : type => @sigT Type (fun x : Type => x)) (field_type (@fst ident type it0) (co_members (@get_co CompSpecs id)))) (fun it0 : prod ident type => (fun t0 : type => if type_is_by_value t0 then @existT Type (fun x : Type => x) val Vundef else @existT Type (fun x : Type => x) unit tt) (field_type (@fst ident type it0) (co_members (@get_co CompSpecs id)))) (co_members (@get_co CompSpecs id))) end | Tunion id a => match @PTree.get composite id (@cenv_cs CompSpecs) with | Some c => (fun t0 : type => if type_is_by_value t0 then @existT Type (fun x : Type => x) val Vundef else @existT Type (fun x : Type => x) unit tt) (Tunion id a) | None => (fun (id0 : positive) (_ : attr) (TVs : @type_induction.FT_aux CompSpecs (fun _ : type => @sigT Type (fun x : Type => x)) id0) => @existT Type (fun x : Type => x) (@compact_sum_sigT_type Type (fun x : Type => x) (@type_induction.decay (prod ident type) (@sigT Type (fun x : Type => x)) (co_members (@get_co CompSpecs id0)) TVs)) (@compact_sum_sigT_value Type (fun x : Type => x) (@type_induction.decay (prod ident type) (@sigT Type (fun x : Type => x)) (co_members (@get_co CompSpecs id0)) TVs))) id a (@type_induction.ListTypeGen (prod ident type) (fun it0 : prod ident type => (fun _ : type => @sigT Type (fun x : Type => x)) (field_type (@fst ident type it0) (co_members (@get_co CompSpecs id)))) (fun it0 : prod ident type => (fun t0 : type => if type_is_by_value t0 then @existT Type (fun x : Type => x) val Vundef else @existT Type (fun x : Type => x) unit tt) (field_type (@fst ident type it0) (co_members (@get_co CompSpecs id)))) (co_members (@get_co CompSpecs id))) end end | S n' => match t as t0 return ((fun _ : type => @sigT Type (fun x : Type => x)) t0) with | Tvoid => (fun t0 : type => if type_is_by_value t0 then @existT Type (fun x : Type => x) val Vundef else @existT Type (fun x : Type => x) unit tt) Tvoid | Tint i s a => (fun t0 : type => if type_is_by_value t0 then @existT Type (fun x : Type => x) val Vundef else @existT Type (fun x : Type => x) unit tt) (Tint i s a) | Tlong s a => (fun t0 : type => if type_is_by_value t0 then @existT Type (fun x : Type => x) val Vundef else @existT Type (fun x : Type => x) unit tt) (Tlong s a) | Tfloat f a => (fun t0 : type => if type_is_by_value t0 then @existT Type (fun x : Type => x) val Vundef else @existT Type (fun x : Type => x) unit tt) (Tfloat f a) | Tpointer t0 a => (fun t1 : type => if type_is_by_value t1 then @existT Type (fun x : Type => x) val Vundef else @existT Type (fun x : Type => x) unit tt) (Tpointer t0 a) | Tarray t0 n0 a => (fun (t1 : type) (n1 : Z) (_ : attr) (TV : (fun _ : type => @sigT Type (fun x : Type => x)) t1) => @existT Type (fun x : Type => x) (list (@projT1 Type (fun x : Type => x) TV)) (@list_repeat (@projT1 Type (fun x : Type => x) TV) (Z.to_nat n1) (@projT2 Type (fun x : Type => x) TV))) t0 n0 a (type_func_rec n' t0) | Tfunction t0 t1 c => (fun t2 : type => if type_is_by_value t2 then @existT Type (fun x : Type => x) val Vundef else @existT Type (fun x : Type => x) unit tt) (Tfunction t0 t1 c) | Tstruct id a => (fun (id0 : positive) (_ : attr) (TVs : @type_induction.FT_aux CompSpecs (fun _ : type => @sigT Type (fun x : Type => x)) id0) => @existT Type (fun x : Type => x) (@compact_prod_sigT_type Type (fun x : Type => x) (@type_induction.decay (prod ident type) (@sigT Type (fun x : Type => x)) (co_members (@get_co CompSpecs id0)) TVs)) (@compact_prod_sigT_value Type (fun x : Type => x) (@type_induction.decay (prod ident type) (@sigT Type (fun x : Type => x)) (co_members (@get_co CompSpecs id0)) TVs))) id a (@type_induction.ListTypeGen (prod ident type) (fun it0 : prod ident type => (fun _ : type => @sigT Type (fun x : Type => x)) (field_type (@fst ident type it0) (co_members (@get_co CompSpecs id)))) (fun it0 : prod ident type => type_func_rec n' (field_type (@fst ident type it0) (co_members (@get_co CompSpecs id)))) (co_members (@get_co CompSpecs id))) | Tunion id a => (fun (id0 : positive) (_ : attr) (TVs : @type_induction.FT_aux CompSpecs (fun _ : type => @sigT Type (fun x : Type => x)) id0) => @existT Type (fun x : Type => x) (@compact_sum_sigT_type Type (fun x : Type => x) (@type_induction.decay (prod ident type) (@sigT Type (fun x : Type => x)) (co_members (@get_co CompSpecs id0)) TVs)) (@compact_sum_sigT_value Type (fun x : Type => x) (@type_induction.decay (prod ident type) (@sigT Type (fun x : Type => x)) (co_members (@get_co CompSpecs id0)) TVs))) id a (@type_induction.ListTypeGen (prod ident type) (fun it0 : prod ident type => (fun _ : type => @sigT Type (fun x : Type => x)) (field_type (@fst ident type it0) (co_members (@get_co CompSpecs id)))) (fun it0 : prod ident type => type_func_rec n' (field_type (@fst ident type it0) (co_members (@get_co CompSpecs id)))) (co_members (@get_co CompSpecs id))) end end) (co_rank (Build_composite Struct (@cons (prod ident type) (@pair ident type _data tint) (@cons (prod ident type) (@pair ident type _next (tptr (Tstruct _elem noattr))) (@nil (prod ident type)))) noattr (Zpos (xO (xO (xO xH)))) (Zpos (xO (xO xH))) O (Zgeb0_ge0 (Zpos (xO (xO (xO xH)))) (@eq_refl bool (Z.geb (Zpos (xO (xO (xO xH)))) Z0))) (prove_alignof_two_p (Zpos (xO (xO xH))) (@eq_refl Z (Zpos (xO (xO xH))))) (prove_Zdivide (Zpos (xO (xO xH))) (Zpos (xO (xO (xO xH)))) (@eq_refl Z (Zpos (xO (xO (xO xH)))))))) (field_type (@fst ident type it) (co_members (@get_co CompSpecs _elem)))) (@pair ident type _data tint)) (@sigT Type (fun x : Type => x)) (@f_equal (list Type) Type (fun e : list Type => match e with | nil => (fun it : prod ident type => (fun _ : type => @sigT Type (fun x : Type => x)) (field_type (@fst ident type it) (co_members (@get_co CompSpecs _elem)))) (@pair ident type _data tint) | cons T l => T end) (@cons Type ((fun it : prod ident type => (fun _ : type => @sigT Type (fun x : Type => x)) (field_type (@fst ident type it) (co_members (@get_co CompSpecs _elem)))) (@pair ident type _data tint)) (@map (prod ident type) Type (fun it : prod ident type => (fun _ : type => @sigT Type (fun x : Type => x)) (field_type (@fst ident type it) (co_members (@get_co CompSpecs _elem)))) (@cons (prod ident type) (@pair ident type _next (tptr (Tstruct _elem noattr))) (@nil (prod ident type))))) (@map (prod ident type) Type (fun _ : prod ident type => @sigT Type (fun x : Type => x)) (@cons (prod ident type) (@pair ident type _data tint) (@cons (prod ident type) (@pair ident type _next (tptr (Tstruct _elem noattr))) (@nil (prod ident type))))) (@eq_refl (list Type) (@map (prod ident type) Type (fun _ : prod ident type => @sigT Type (fun x : Type => x)) (@cons (prod ident type) (@pair ident type _data tint) (@cons (prod ident type) (@pair ident type _next (tptr (Tstruct _elem noattr))) (@nil (prod ident type))))))) in (fun x : Type => x) t) val i v) p) (@sepcon mpred Nveric Sveric (@list_cell CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS sh i p) (@field_at CompSpecs sh t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) v p)) *)
unfold_data_at (data_at _ _ _ _).
(* Goal: @eq mpred (@andp mpred Nveric (@prop mpred Nveric (@field_compatible CompSpecs t_struct_elem (@cons gfield (StructField _data) (@nil gfield)) p)) (at_offset (@data_at_rec CompSpecs sh (@nested_field_type CompSpecs t_struct_elem (@cons gfield (StructField _data) (@nil gfield))) i) (@nested_field_offset CompSpecs t_struct_elem (@cons gfield (StructField _data) (@nil gfield))) p)) (@andp mpred Nveric (@prop mpred Nveric (@field_compatible CompSpecs (@list_struct CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS) (@nil gfield) p)) (@struct_pred (@all_but_link _next (@list_fields CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS)) (fun it : prod ident type => @reptype CompSpecs (field_type (@fst ident type it) (@list_fields CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS))) (fun (it : prod ident type) (v : @reptype CompSpecs (field_type (@fst ident type it) (@list_fields CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS))) => withspacer sh (Z.add (field_offset (@cenv_cs CompSpecs) (@fst ident type it) (@list_fields CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS)) (@sizeof (@cenv_cs CompSpecs) (field_type (@fst ident type it) (@list_fields CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS)))) (field_offset_next (@cenv_cs CompSpecs) (@fst ident type it) (@list_fields CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS) (co_sizeof (@get_co CompSpecs _elem))) (at_offset (@data_at_rec CompSpecs sh (field_type (@fst ident type it) (@list_fields CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS)) v) (field_offset (@cenv_cs CompSpecs) (@fst ident type it) (@list_fields CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS)))) i p)) *)
f_equal.
(* Goal: @eq mpred (@field_at CompSpecs sh t_struct_elem (@cons gfield (StructField _data) (@nil gfield)) i p) (@list_cell CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS sh i p) *)
unfold field_at, list_cell.
(* Goal: @eq mpred (@andp mpred Nveric (@prop mpred Nveric (@field_compatible CompSpecs t_struct_elem (@cons gfield (StructField _data) (@nil gfield)) p)) (at_offset (@data_at_rec CompSpecs sh (@nested_field_type CompSpecs t_struct_elem (@cons gfield (StructField _data) (@nil gfield))) i) (@nested_field_offset CompSpecs t_struct_elem (@cons gfield (StructField _data) (@nil gfield))) p)) (@andp mpred Nveric (@prop mpred Nveric (@field_compatible CompSpecs (@list_struct CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS) (@nil gfield) p)) (@struct_pred (@all_but_link _next (@list_fields CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS)) (fun it : prod ident type => @reptype CompSpecs (field_type (@fst ident type it) (@list_fields CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS))) (fun (it : prod ident type) (v : @reptype CompSpecs (field_type (@fst ident type it) (@list_fields CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS))) => withspacer sh (Z.add (field_offset (@cenv_cs CompSpecs) (@fst ident type it) (@list_fields CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS)) (@sizeof (@cenv_cs CompSpecs) (field_type (@fst ident type it) (@list_fields CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS)))) (field_offset_next (@cenv_cs CompSpecs) (@fst ident type it) (@list_fields CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS) (co_sizeof (@get_co CompSpecs _elem))) (at_offset (@data_at_rec CompSpecs sh (field_type (@fst ident type it) (@list_fields CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS)) v) (field_offset (@cenv_cs CompSpecs) (@fst ident type it) (@list_fields CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS)))) i p)) *)
autorewrite with gather_prop.
(* Goal: @eq mpred (@andp mpred Nveric (@prop mpred Nveric (@field_compatible CompSpecs t_struct_elem (@cons gfield (StructField _data) (@nil gfield)) p)) (at_offset (@data_at_rec CompSpecs sh (@nested_field_type CompSpecs t_struct_elem (@cons gfield (StructField _data) (@nil gfield))) i) (@nested_field_offset CompSpecs t_struct_elem (@cons gfield (StructField _data) (@nil gfield))) p)) (@andp mpred Nveric (@prop mpred Nveric (@field_compatible CompSpecs (@list_struct CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS) (@nil gfield) p)) (@struct_pred (@all_but_link _next (@list_fields CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS)) (fun it : prod ident type => @reptype CompSpecs (field_type (@fst ident type it) (@list_fields CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS))) (fun (it : prod ident type) (v : @reptype CompSpecs (field_type (@fst ident type it) (@list_fields CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS))) => withspacer sh (Z.add (field_offset (@cenv_cs CompSpecs) (@fst ident type it) (@list_fields CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS)) (@sizeof (@cenv_cs CompSpecs) (field_type (@fst ident type it) (@list_fields CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS)))) (field_offset_next (@cenv_cs CompSpecs) (@fst ident type it) (@list_fields CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS) (co_sizeof (@get_co CompSpecs _elem))) (at_offset (@data_at_rec CompSpecs sh (field_type (@fst ident type it) (@list_fields CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS)) v) (field_offset (@cenv_cs CompSpecs) (@fst ident type it) (@list_fields CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS)))) i p)) *)
f_equal.
(* Goal: @eq mpred (@prop mpred Nveric (@field_compatible CompSpecs t_struct_elem (@cons gfield (StructField _data) (@nil gfield)) p)) (@prop mpred Nveric (@field_compatible CompSpecs (@list_struct CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS) (@nil gfield) p)) *)
apply ND_prop_ext.
(* Goal: iff (@field_compatible CompSpecs t_struct_elem (@cons gfield (StructField _data) (@nil gfield)) p) (@field_compatible CompSpecs (@list_struct CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS) (@nil gfield) p) *)
rewrite field_compatible_cons; simpl.
(* Goal: iff (and (in_members _data (@cons (prod ident type) (@pair ident type _data tint) (@cons (prod ident type) (@pair ident type _next (tptr (Tstruct _elem noattr))) (@nil (prod ident type))))) (@field_compatible CompSpecs t_struct_elem (@nil gfield) p)) (@field_compatible CompSpecs (@list_struct CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS) (@nil gfield) p) *)
intuition.
(* Goal: in_members _data (@cons (prod ident type) (@pair ident type _data tint) (@cons (prod ident type) (@pair ident type _next (tptr (Tstruct _elem noattr))) (@nil (prod ident type)))) *)
left; auto.
Qed.

Definition surely_malloc_spec :=
  DECLARE _surely_malloc
   WITH t:type, gv: globals
   PRE [ _n OF tuint ]
       PROP (0 <= sizeof t <= Int.max_unsigned;
                complete_legal_cosu_type t = true;
                natural_aligned natural_alignment t = true)
       LOCAL (temp _n (Vint (Int.repr (sizeof t))); gvars gv)
       SEP (mem_mgr gv)
    POST [ tptr tvoid ] EX p:_,
       PROP ()
       LOCAL (temp ret_temp p)
       SEP (mem_mgr gv; malloc_token Ews t p * data_at_ Ews t p).

Definition fifo_body (contents: list val) (hd tl : val) :=
     (if isnil contents
      then (!!(hd=nullval) && emp)
      else (EX prefix: list val, EX last: val,
              !!(contents = prefix++last::nil)
            &&  (lseg QS Ews prefix hd tl
                   * malloc_token Ews t_struct_elem tl
                   * data_at Ews t_struct_elem (last, nullval) tl)))%logic.

Definition fifo (contents: list val) (p: val) : mpred :=
  EX ht: (val*val), let (hd,tl) := ht in
      !! is_pointer_or_null hd && !! is_pointer_or_null tl &&
      data_at Ews t_struct_fifo (hd, tl) p * malloc_token Ews t_struct_fifo p *
      fifo_body contents hd tl.

Definition fifo_new_spec :=
 DECLARE _fifo_new
  WITH gv: globals
  PRE  [  ]
       PROP() LOCAL(gvars gv) SEP (mem_mgr gv)
  POST [ (tptr t_struct_fifo) ]
    EX v:val, PROP() LOCAL(temp ret_temp v) SEP (mem_mgr gv; fifo nil v).

Definition fifo_put_spec :=
 DECLARE _fifo_put
  WITH q: val, contents: list val, p: val, last: val
  PRE  [ _Q OF (tptr t_struct_fifo) , _p OF (tptr t_struct_elem) ]
          PROP () LOCAL (temp _Q q; temp _p p)
          SEP (fifo contents q;
                 malloc_token Ews t_struct_elem p;
                 data_at Ews t_struct_elem (last,Vundef) p)
  POST [ tvoid ]
          PROP() LOCAL() SEP (fifo (contents++(last :: nil)) q).

Definition fifo_empty_spec :=
 DECLARE _fifo_empty
  WITH q: val, contents: list val
  PRE  [ _Q OF (tptr t_struct_fifo) ]
     PROP() LOCAL (temp _Q q) SEP(fifo contents q)
  POST [ tint ]
      PROP ()
      LOCAL(temp ret_temp (if isnil contents then Vtrue else Vfalse))
      SEP (fifo (contents) q).

Definition fifo_get_spec :=
 DECLARE _fifo_get
  WITH q: val, contents: list val, first: val
  PRE  [ _Q OF (tptr t_struct_fifo) ]
       PROP() LOCAL (temp _Q q) SEP (fifo (first :: contents) q)
  POST [ (tptr t_struct_elem) ]
      EX p:val,
       PROP ()
       LOCAL(temp ret_temp p)
       SEP (fifo contents q;
              malloc_token Ews t_struct_elem p;
              data_at Ews t_struct_elem (first,Vundef) p).

Definition make_elem_spec :=
 DECLARE _make_elem
  WITH i: int, gv: globals
  PRE  [ _data OF tint ]
        PROP() LOCAL(temp _data (Vint i); gvars gv) SEP(mem_mgr gv)
  POST [ (tptr t_struct_elem) ]
    EX p:val,
       PROP()
       LOCAL (temp ret_temp p)
       SEP (mem_mgr gv; 
              malloc_token Ews t_struct_elem p;
              data_at Ews t_struct_elem (Vint i, Vundef) p).

Definition main_spec :=
 DECLARE _main
  WITH gv: globals
  PRE  [] main_pre prog nil gv
  POST [ tint ]
       PROP() LOCAL (temp ret_temp (Vint (Int.repr 1))) SEP(TT).

Definition Gprog : funspecs :=
  ltac:(with_library prog
    [surely_malloc_spec; fifo_new_spec; fifo_put_spec;
     fifo_empty_spec; fifo_get_spec; make_elem_spec;
     main_spec]).

Lemma body_surely_malloc: semax_body Vprog Gprog f_surely_malloc surely_malloc_spec.
Proof.
(* Goal: semax_body Vprog Gprog CompSpecs f_make_elem make_elem_spec *)
  start_function.
  forward_call (* p = malloc(n); *)
     (t,gv).
(* Goal: semax CompSpecs Espec Delta (@exp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) val (fun vret : val => PROPx (@nil Prop) (LOCALx (@cons localdef (temp _p vret) (@cons localdef (temp _data (Vint i)) (@cons localdef (gvars gv) (@nil localdef)))) (SEPx (@cons mpred (mem_mgr gv) (@cons mpred (@sepcon mpred Nveric Sveric (@malloc_token CompSpecs Ews t_struct_elem vret) (@data_at_ CompSpecs Ews t_struct_elem vret)) (@nil mpred))))))) (Ssequence (Sassign (Efield (Ederef (Etempvar _p (tptr (Tstruct _elem noattr))) (Tstruct _elem noattr)) _data tint) (Etempvar _data tint)) MORE_COMMANDS) POSTCONDITION *)
  Intros p.
  forward_if
  (PROP ( )
   LOCAL (temp _p p)
   SEP (mem_mgr gv; malloc_token Ews t p * data_at_ Ews t p)).
*
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _p p) (@cons localdef (temp _n (Vint (Int.repr (@sizeof (@cenv_cs CompSpecs) t)))) (@cons localdef (gvars gv) (@nil localdef)))) (SEPx (@cons mpred (mem_mgr gv) (@cons mpred (if @eq_dec val Memory.EqDec_val p nullval then @emp mpred Nveric Sveric else @sepcon mpred Nveric Sveric (@malloc_token CompSpecs Ews t p) (@data_at_ CompSpecs Ews t p)) (@nil mpred)))))) Sskip POSTCONDITION *)
  if_tac.
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (tc_environ Delta)) (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _p p) (@cons localdef (temp _n (Vint (Int.repr (@sizeof (@cenv_cs CompSpecs) t)))) (@cons localdef (gvars gv) (@nil localdef)))) (SEPx (@cons mpred (mem_mgr gv) (@cons mpred (@emp mpred Nveric Sveric) (@nil mpred))))))) (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _p p) (@nil localdef)) (SEPx (@cons mpred (mem_mgr gv) (@cons mpred (@sepcon mpred Nveric Sveric (@malloc_token CompSpecs Ews t p) (@data_at_ CompSpecs Ews t p)) (@nil mpred)))))) *)
    subst p. entailer!.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (mem_mgr gv) (@malloc_token CompSpecs Ews t_struct_elem p)) (@data_at CompSpecs Ews t_struct_elem (@pair val val (Vint i) Vundef) p)) (@andp mpred Nveric (@prop mpred Nveric (@eq val p p)) (@sepcon mpred Nveric Sveric (mem_mgr gv) (@sepcon mpred Nveric Sveric (@malloc_token CompSpecs Ews t_struct_elem p) (@data_at CompSpecs Ews t_struct_elem (@pair val val (Vint i) Vundef) p)))) *)
    entailer!.
*
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _p p) (@cons localdef (temp _n (Vint (Int.repr (@sizeof (@cenv_cs CompSpecs) t)))) (@cons localdef (gvars gv) (@nil localdef)))) (SEPx (@cons mpred (mem_mgr gv) (@cons mpred (if @eq_dec val Memory.EqDec_val p nullval then @emp mpred Nveric Sveric else @sepcon mpred Nveric Sveric (@malloc_token CompSpecs Ews t p) (@data_at_ CompSpecs Ews t p)) (@nil mpred)))))) (Scall (@None ident) (Evar _exit (Tfunction (Tcons tint Tnil) tvoid cc_default)) (@cons expr (Econst_int (Int.repr (Zpos xH)) tint) (@nil expr))) POSTCONDITION *)
    forward_call tt.
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (tc_environ Delta)) (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _p p) (@cons localdef (temp _n (Vint (Int.repr (@sizeof (@cenv_cs CompSpecs) t)))) (@cons localdef (gvars gv) (@nil localdef)))) (SEPx (@cons mpred (mem_mgr gv) (@cons mpred (if @eq_dec val Memory.EqDec_val p nullval then @emp mpred Nveric Sveric else @sepcon mpred Nveric Sveric (@malloc_token CompSpecs Ews t p) (@data_at_ CompSpecs Ews t p)) (@nil mpred))))))) (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _p p) (@nil localdef)) (SEPx (@cons mpred (mem_mgr gv) (@cons mpred (@sepcon mpred Nveric Sveric (@malloc_token CompSpecs Ews t p) (@data_at_ CompSpecs Ews t p)) (@nil mpred)))))) *)
    contradiction.
*
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _p p) (@cons localdef (temp _n (Vint (Int.repr (@sizeof (@cenv_cs CompSpecs) t)))) (@cons localdef (gvars gv) (@nil localdef)))) (SEPx (@cons mpred (mem_mgr gv) (@cons mpred (if @eq_dec val Memory.EqDec_val p nullval then @emp mpred Nveric Sveric else @sepcon mpred Nveric Sveric (@malloc_token CompSpecs Ews t p) (@data_at_ CompSpecs Ews t p)) (@nil mpred)))))) Sskip POSTCONDITION *)
    if_tac.
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (tc_environ Delta)) (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _p p) (@cons localdef (temp _n (Vint (Int.repr (@sizeof (@cenv_cs CompSpecs) t)))) (@cons localdef (gvars gv) (@nil localdef)))) (SEPx (@cons mpred (mem_mgr gv) (@cons mpred (@emp mpred Nveric Sveric) (@nil mpred))))))) (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _p p) (@nil localdef)) (SEPx (@cons mpred (mem_mgr gv) (@cons mpred (@sepcon mpred Nveric Sveric (@malloc_token CompSpecs Ews t p) (@data_at_ CompSpecs Ews t p)) (@nil mpred)))))) *)
    + forward. subst p. congruence.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (mem_mgr gv) (@malloc_token CompSpecs Ews t_struct_elem p)) (@data_at CompSpecs Ews t_struct_elem (@pair val val (Vint i) Vundef) p)) (@andp mpred Nveric (@prop mpred Nveric (@eq val p p)) (@sepcon mpred Nveric Sveric (mem_mgr gv) (@sepcon mpred Nveric Sveric (@malloc_token CompSpecs Ews t_struct_elem p) (@data_at CompSpecs Ews t_struct_elem (@pair val val (Vint i) Vundef) p)))) *)
    + Intros. forward. entailer!.
*
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (mem_mgr gv) (@malloc_token CompSpecs Ews t_struct_elem p)) (@data_at CompSpecs Ews t_struct_elem (@pair val val (Vint i) Vundef) p)) (@andp mpred Nveric (@prop mpred Nveric (@eq val p p)) (@sepcon mpred Nveric Sveric (mem_mgr gv) (@sepcon mpred Nveric Sveric (@malloc_token CompSpecs Ews t_struct_elem p) (@data_at CompSpecs Ews t_struct_elem (@pair val val (Vint i) Vundef) p)))) *)
  forward. Exists p; entailer!.
Qed.

Lemma fifo_isptr: forall al q, fifo al q |-- !! isptr q.
Proof.
(* Goal: forall (al : list val) (q : val), @derives mpred Nveric (fifo al q) (@prop mpred Nveric (isptr q)) *)
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 (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Ews t_struct_fifo (@pair val val x tl) q) (@malloc_token CompSpecs Ews t_struct_fifo q)) (@malloc_token CompSpecs Ews t_struct_elem hd)) (@list_cell CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS Ews v hd)) (@field_at CompSpecs Ews (@list_struct CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS) (@cons gfield (StructField _next) (@nil gfield)) x hd)) (@lseg CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS Ews prefix x tl)) (@malloc_token CompSpecs Ews t_struct_elem tl)) (@data_at CompSpecs Ews t_struct_elem (@pair val val last nullval) tl)) (@andp mpred Nveric (@prop mpred Nveric (@eq val hd hd)) (@sepcon mpred Nveric Sveric (fifo (@app val prefix (@cons val last (@nil val))) q) (@sepcon mpred Nveric Sveric (@malloc_token CompSpecs Ews t_struct_elem hd) (@data_at CompSpecs Ews t_struct_elem (@pair val val v Vundef) hd)))) *)
 unfold fifo, fifo_body.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (mem_mgr gv) (@malloc_token CompSpecs Ews t_struct_elem p)) (@data_at CompSpecs Ews t_struct_elem (@pair val val (Vint i) Vundef) p)) (@andp mpred Nveric (@prop mpred Nveric (@eq val p p)) (@sepcon mpred Nveric Sveric (mem_mgr gv) (@sepcon mpred Nveric Sveric (@malloc_token CompSpecs Ews t_struct_elem p) (@data_at CompSpecs Ews t_struct_elem (@pair val val (Vint i) Vundef) p)))) *)
 if_tac; entailer; destruct ht; entailer!.
Qed.

Hint Resolve fifo_isptr : saturate_local.

Lemma body_fifo_empty: semax_body Vprog Gprog f_fifo_empty fifo_empty_spec.
Proof.
(* Goal: semax_body Vprog Gprog CompSpecs f_make_elem make_elem_spec *)
start_function.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _Q q) (@nil localdef)) (SEPx (@cons mpred (fifo contents q) (@nil mpred))))) (Ssequence (Sset _h (Efield (Ederef (Etempvar _Q (tptr (Tstruct _fifo noattr))) (Tstruct _fifo noattr)) _head (tptr (Tstruct _elem noattr)))) MORE_COMMANDS) POSTCONDITION *)
unfold fifo.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _Q q) (@nil localdef)) (SEPx (@cons mpred (@exp mpred Nveric (prod val val) (fun ht : prod val val => let (hd, tl) := ht in @sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@andp mpred Nveric (@andp mpred Nveric (@prop mpred Nveric (is_pointer_or_null hd)) (@prop mpred Nveric (is_pointer_or_null tl))) (@data_at CompSpecs Ews t_struct_fifo (@pair val val hd tl) q)) (@malloc_token CompSpecs Ews t_struct_fifo q)) (if @isnil val (@cons val first contents) then @andp mpred Nveric (@prop mpred Nveric (@eq val hd nullval)) (@emp mpred Nveric Sveric) else @exp mpred Nveric (list val) (fun prefix : list val => @exp mpred Nveric val (fun last : val => @andp mpred Nveric (@prop mpred Nveric (@eq (list val) (@cons val first contents) (@app val prefix (@cons val last (@nil val))))) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@lseg CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS Ews prefix hd tl) (@malloc_token CompSpecs Ews t_struct_elem tl)) (@data_at CompSpecs Ews t_struct_elem (@pair val val last nullval) tl))))))) (@nil mpred))))) (Ssequence (Sset _h (Efield (Ederef (Etempvar _Q (tptr (Tstruct _fifo noattr))) (Tstruct _fifo noattr)) _head (tptr (Tstruct _elem noattr)))) MORE_COMMANDS) POSTCONDITION *)
Intros ht; destruct ht as [hd tl].
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _h hd) (@cons localdef (temp _Q q) (@nil localdef))) (SEPx (@cons mpred (@data_at CompSpecs Ews t_struct_fifo (@pair val val hd tl) q) (@cons mpred (@malloc_token CompSpecs Ews t_struct_fifo q) (@cons mpred (@andp mpred Nveric (@prop mpred Nveric (ptr_eq hd tl)) (@emp mpred Nveric Sveric)) (@cons mpred (@malloc_token CompSpecs Ews t_struct_elem tl) (@cons mpred (@data_at CompSpecs Ews t_struct_elem (@pair val val last nullval) tl) (@nil mpred))))))))) (Ssequence (Sset _n (Efield (Ederef (Etempvar _h (tptr (Tstruct _elem noattr))) (Tstruct _elem noattr)) _next (tptr (Tstruct _elem noattr)))) MORE_COMMANDS) POSTCONDITION *)
Intros.
forward. (* h = Q->head; *)
forward. (* return (h == NULL); *)
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Ews t_struct_fifo (@pair val val hd tl) q) (@malloc_token CompSpecs Ews t_struct_fifo q)) (fifo_body contents hd tl)) (denote_tc_test_eq hd (Vint (Int.repr Z0))) *)
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Ews t_struct_fifo (@pair val val hd tl) q) (@malloc_token CompSpecs Ews t_struct_fifo q)) (fifo_body contents hd tl)) (@andp mpred Nveric (@prop mpred Nveric (@eq val (force_val (@sem_binary_operation' CompSpecs Oeq (typeof (Etempvar _h (tptr (Tstruct _elem noattr)))) (typeof (Ecast (Econst_int (Int.repr Z0) tint) (tptr tvoid))) hd (eval_cast (typeof (Econst_int (Int.repr Z0) tint)) (tptr tvoid) (Vint (Int.repr Z0))))) (if @isnil val contents then Vtrue else Vfalse))) (fifo contents q)) *)
{
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Ews t_struct_fifo (@pair val val x tl) q) (@malloc_token CompSpecs Ews t_struct_fifo q)) (@malloc_token CompSpecs Ews t_struct_elem hd)) (@list_cell CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS Ews v hd)) (@field_at CompSpecs Ews (@list_struct CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS) (@cons gfield (StructField _next) (@nil gfield)) x hd)) (@lseg CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS Ews prefix x tl)) (@malloc_token CompSpecs Ews t_struct_elem tl)) (@data_at CompSpecs Ews t_struct_elem (@pair val val last nullval) tl)) (@andp mpred Nveric (@prop mpred Nveric (@eq val hd hd)) (@sepcon mpred Nveric Sveric (fifo (@app val prefix (@cons val last (@nil val))) q) (@sepcon mpred Nveric Sveric (@malloc_token CompSpecs Ews t_struct_elem hd) (@data_at CompSpecs Ews t_struct_elem (@pair val val v Vundef) hd)))) *)
unfold fifo, fifo_body.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _t tl) (@cons localdef (temp _h hd) (@cons localdef (temp _Q q) (@cons localdef (temp _p p) (@nil localdef))))) (SEPx (@cons mpred (@data_at CompSpecs Ews t_struct_fifo (@pair val val hd tl) q) (@cons mpred (@malloc_token CompSpecs Ews t_struct_fifo q) (@cons mpred (if @isnil val contents then @andp mpred Nveric (@prop mpred Nveric (@eq val hd nullval)) (@emp mpred Nveric Sveric) else @exp mpred Nveric (list val) (fun prefix : list val => @exp mpred Nveric val (fun last : val => @andp mpred Nveric (@prop mpred Nveric (@eq (list val) contents (@app val prefix (@cons val last (@nil val))))) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@lseg CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS Ews prefix hd tl) (@malloc_token CompSpecs Ews t_struct_elem tl)) (@data_at CompSpecs Ews t_struct_elem (@pair val val last nullval) tl))))) (@cons mpred (@malloc_token CompSpecs Ews t_struct_elem p) (@cons mpred (@data_at CompSpecs Ews t_struct_elem (@pair val val last (Vint (Int.repr Z0))) p) (@nil mpred))))))))) (Ssequence (Sassign (Efield (Ederef (Etempvar _t (tptr (Tstruct _elem noattr))) (Tstruct _elem noattr)) _next (tptr (Tstruct _elem noattr))) (Etempvar _p (tptr (Tstruct _elem noattr)))) MORE_COMMANDS) POSTCONDITION *)
destruct (isnil contents).
+ normalize; auto with valid_pointer.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (mem_mgr gv) (@malloc_token CompSpecs Ews t_struct_elem p)) (@data_at CompSpecs Ews t_struct_elem (@pair val val (Vint i) Vundef) p)) (@andp mpred Nveric (@prop mpred Nveric (@eq val p p)) (@sepcon mpred Nveric Sveric (mem_mgr gv) (@sepcon mpred Nveric Sveric (@malloc_token CompSpecs Ews t_struct_elem p) (@data_at CompSpecs Ews t_struct_elem (@pair val val (Vint i) Vundef) p)))) *)
+ entailer!.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (mem_mgr gv) (@malloc_token CompSpecs Ews t_struct_elem p)) (@data_at CompSpecs Ews t_struct_elem (@pair val val (Vint i) Vundef) p)) (@andp mpred Nveric (@prop mpred Nveric (@eq val p p)) (@sepcon mpred Nveric Sveric (mem_mgr gv) (@sepcon mpred Nveric Sveric (@malloc_token CompSpecs Ews t_struct_elem p) (@data_at CompSpecs Ews t_struct_elem (@pair val val (Vint i) Vundef) p)))) *)
  destruct hd; inv PNhd; entailer!.
}
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Ews t_struct_fifo (@pair val val x tl) q) (@malloc_token CompSpecs Ews t_struct_fifo q)) (@malloc_token CompSpecs Ews t_struct_elem hd)) (@list_cell CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS Ews v hd)) (@field_at CompSpecs Ews (@list_struct CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS) (@cons gfield (StructField _next) (@nil gfield)) x hd)) (@lseg CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS Ews prefix x tl)) (@malloc_token CompSpecs Ews t_struct_elem tl)) (@data_at CompSpecs Ews t_struct_elem (@pair val val last nullval) tl)) (@andp mpred Nveric (@prop mpred Nveric (@eq val hd hd)) (@sepcon mpred Nveric Sveric (fifo (@app val prefix (@cons val last (@nil val))) q) (@sepcon mpred Nveric Sveric (@malloc_token CompSpecs Ews t_struct_elem hd) (@data_at CompSpecs Ews t_struct_elem (@pair val val v Vundef) hd)))) *)
unfold fifo, fifo_body.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Ews t_struct_fifo (@pair val val hd tl) q) (@malloc_token CompSpecs Ews t_struct_fifo q)) (if @isnil val contents then @andp mpred Nveric (@prop mpred Nveric (@eq val hd nullval)) (@emp mpred Nveric Sveric) else @exp mpred Nveric (list val) (fun prefix : list val => @exp mpred Nveric val (fun last : val => @andp mpred Nveric (@prop mpred Nveric (@eq (list val) contents (@app val prefix (@cons val last (@nil val))))) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@lseg CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS Ews prefix hd tl) (@malloc_token CompSpecs Ews t_struct_elem tl)) (@data_at CompSpecs Ews t_struct_elem (@pair val val last nullval) tl)))))) (@andp mpred Nveric (@prop mpred Nveric (@eq val (force_val (@sem_binary_operation' CompSpecs Oeq (typeof (Etempvar _h (tptr (Tstruct _elem noattr)))) (typeof (Ecast (Econst_int (Int.repr Z0) tint) (tptr tvoid))) hd (eval_cast (typeof (Econst_int (Int.repr Z0) tint)) (tptr tvoid) (Vint (Int.repr Z0))))) (if @isnil val contents then Vtrue else Vfalse))) (@exp mpred Nveric (prod val val) (fun ht : prod val val => let (hd, tl) := ht in @sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@andp mpred Nveric (@andp mpred Nveric (@prop mpred Nveric (is_pointer_or_null hd)) (@prop mpred Nveric (is_pointer_or_null tl))) (@data_at CompSpecs Ews t_struct_fifo (@pair val val hd tl) q)) (@malloc_token CompSpecs Ews t_struct_fifo q)) (if @isnil val contents then @andp mpred Nveric (@prop mpred Nveric (@eq val hd nullval)) (@emp mpred Nveric Sveric) else @exp mpred Nveric (list val) (fun prefix : list val => @exp mpred Nveric val (fun last : val => @andp mpred Nveric (@prop mpred Nveric (@eq (list val) contents (@app val prefix (@cons val last (@nil val))))) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@lseg CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS Ews prefix hd tl) (@malloc_token CompSpecs Ews t_struct_elem tl)) (@data_at CompSpecs Ews t_struct_elem (@pair val val last nullval) tl)))))))) *)
Exists (hd,tl).
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _t tl) (@cons localdef (temp _h hd) (@cons localdef (temp _Q q) (@cons localdef (temp _p p) (@nil localdef))))) (SEPx (@cons mpred (@data_at CompSpecs Ews t_struct_fifo (@pair val val hd tl) q) (@cons mpred (@malloc_token CompSpecs Ews t_struct_fifo q) (@cons mpred (if @isnil val contents then @andp mpred Nveric (@prop mpred Nveric (@eq val hd nullval)) (@emp mpred Nveric Sveric) else @exp mpred Nveric (list val) (fun prefix : list val => @exp mpred Nveric val (fun last : val => @andp mpred Nveric (@prop mpred Nveric (@eq (list val) contents (@app val prefix (@cons val last (@nil val))))) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@lseg CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS Ews prefix hd tl) (@malloc_token CompSpecs Ews t_struct_elem tl)) (@data_at CompSpecs Ews t_struct_elem (@pair val val last nullval) tl))))) (@cons mpred (@malloc_token CompSpecs Ews t_struct_elem p) (@cons mpred (@data_at CompSpecs Ews t_struct_elem (@pair val val last (Vint (Int.repr Z0))) p) (@nil mpred))))))))) (Ssequence (Sassign (Efield (Ederef (Etempvar _t (tptr (Tstruct _elem noattr))) (Tstruct _elem noattr)) _next (tptr (Tstruct _elem noattr))) (Etempvar _p (tptr (Tstruct _elem noattr)))) MORE_COMMANDS) POSTCONDITION *)
destruct (isnil contents).
* entailer!.
* Intros prefix last.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Ews t_struct_fifo (@pair val val x tl) q) (@malloc_token CompSpecs Ews t_struct_fifo q)) (@malloc_token CompSpecs Ews t_struct_elem hd)) (@list_cell CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS Ews v hd)) (@field_at CompSpecs Ews (@list_struct CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS) (@cons gfield (StructField _next) (@nil gfield)) x hd)) (@lseg CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS Ews prefix x tl)) (@malloc_token CompSpecs Ews t_struct_elem tl)) (@data_at CompSpecs Ews t_struct_elem (@pair val val last nullval) tl)) (@andp mpred Nveric (@prop mpred Nveric (@eq val hd hd)) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@andp mpred Nveric (@andp mpred Nveric (@prop mpred Nveric (is_pointer_or_null x)) (@prop mpred Nveric (is_pointer_or_null tl))) (@data_at CompSpecs Ews t_struct_fifo (@pair val val x tl) q)) (@malloc_token CompSpecs Ews t_struct_fifo q)) (@exp mpred Nveric (list val) (fun prefix0 : list val => @exp mpred Nveric val (fun last0 : val => @andp mpred Nveric (@prop mpred Nveric (@eq (list val) (@app val prefix (@cons val last (@nil val))) (@app val prefix0 (@cons val last0 (@nil val))))) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@lseg CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS Ews prefix0 x tl) (@malloc_token CompSpecs Ews t_struct_elem tl)) (@data_at CompSpecs Ews t_struct_elem (@pair val val last0 nullval) tl)))))) (@sepcon mpred Nveric Sveric (@malloc_token CompSpecs Ews t_struct_elem hd) (@data_at CompSpecs Ews t_struct_elem (@pair val val v Vundef) hd)))) *)
Exists prefix last.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Ews t_struct_fifo (@pair val val hd tl) q) (@malloc_token CompSpecs Ews t_struct_fifo q)) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@lseg CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS Ews prefix hd tl) (@malloc_token CompSpecs Ews t_struct_elem tl)) (@data_at CompSpecs Ews t_struct_elem (@pair val val last nullval) tl))) (@andp mpred Nveric (@prop mpred Nveric (and (@eq val (force_val (@sem_binary_operation' CompSpecs Oeq (typeof (Etempvar _h (tptr (Tstruct _elem noattr)))) (typeof (Ecast (Econst_int (Int.repr Z0) tint) (tptr tvoid))) hd (eval_cast (typeof (Econst_int (Int.repr Z0) tint)) (tptr tvoid) (Vint (Int.repr Z0))))) Vfalse) (and (is_pointer_or_null hd) (is_pointer_or_null tl)))) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Ews t_struct_fifo (@pair val val hd tl) q) (@malloc_token CompSpecs Ews t_struct_fifo q)) (@andp mpred Nveric (@prop mpred Nveric (@eq (list val) contents (@app val prefix (@cons val last (@nil val))))) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@lseg CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS Ews prefix hd tl) (@malloc_token CompSpecs Ews t_struct_elem tl)) (@data_at CompSpecs Ews t_struct_elem (@pair val val last nullval) tl))))) *)
  assert_PROP (isptr hd).
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Ews t_struct_fifo (@pair val val hd tl) q) (@malloc_token CompSpecs Ews t_struct_fifo q)) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@lseg CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS Ews prefix hd tl) (@malloc_token CompSpecs Ews t_struct_elem tl)) (@data_at CompSpecs Ews t_struct_elem (@pair val val last nullval) tl))) (@prop mpred Nveric (isptr hd)) *)
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Ews t_struct_fifo (@pair val val hd tl) q) (@malloc_token CompSpecs Ews t_struct_fifo q)) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@lseg CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS Ews prefix hd tl) (@malloc_token CompSpecs Ews t_struct_elem tl)) (@data_at CompSpecs Ews t_struct_elem (@pair val val last nullval) tl))) (@andp mpred Nveric (@prop mpred Nveric (and (@eq val (force_val (@sem_binary_operation' CompSpecs Oeq (typeof (Etempvar _h (tptr (Tstruct _elem noattr)))) (typeof (Ecast (Econst_int (Int.repr Z0) tint) (tptr tvoid))) hd (eval_cast (typeof (Econst_int (Int.repr Z0) tint)) (tptr tvoid) (Vint (Int.repr Z0))))) Vfalse) (and (is_pointer_or_null hd) (is_pointer_or_null tl)))) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Ews t_struct_fifo (@pair val val hd tl) q) (@malloc_token CompSpecs Ews t_struct_fifo q)) (@andp mpred Nveric (@prop mpred Nveric (@eq (list val) contents (@app val prefix (@cons val last (@nil val))))) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@lseg CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS Ews prefix hd tl) (@malloc_token CompSpecs Ews t_struct_elem tl)) (@data_at CompSpecs Ews t_struct_elem (@pair val val last nullval) tl))))) *)
    destruct prefix; entailer.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _h hd) (@cons localdef (temp _Q q) (@nil localdef))) (SEPx (@cons mpred (@data_at CompSpecs Ews t_struct_fifo (@pair val val hd tl) q) (@cons mpred (@malloc_token CompSpecs Ews t_struct_fifo q) (@cons mpred (@lseg CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS Ews (@cons val v prefix) hd tl) (@cons mpred (@malloc_token CompSpecs Ews t_struct_elem tl) (@cons mpred (@data_at CompSpecs Ews t_struct_elem (@pair val val last nullval) tl) (@nil mpred))))))))) (Ssequence (Sset _n (Efield (Ederef (Etempvar _h (tptr (Tstruct _elem noattr))) (Tstruct _elem noattr)) _next (tptr (Tstruct _elem noattr)))) MORE_COMMANDS) POSTCONDITION *)
    rewrite @lseg_cons_eq by auto. Intros y.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Ews t_struct_fifo (@pair val val hd p) q) (@malloc_token CompSpecs Ews t_struct_fifo q)) (@lseg CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS Ews prefix hd tl)) (@malloc_token CompSpecs Ews t_struct_elem tl)) (@data_at CompSpecs Ews t_struct_elem (@pair val val last0 p) tl)) (@malloc_token CompSpecs Ews t_struct_elem p)) (@data_at CompSpecs Ews t_struct_elem (@pair val val last (Vint (Int.repr Z0))) p)) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@andp mpred Nveric (@andp mpred Nveric (@prop mpred Nveric (is_pointer_or_null hd)) (@prop mpred Nveric (is_pointer_or_null p))) (@data_at CompSpecs Ews t_struct_fifo (@pair val val hd p) q)) (@malloc_token CompSpecs Ews t_struct_fifo q)) (@andp mpred Nveric (@prop mpred Nveric (@eq (list val) (@app val (@app val prefix (@cons val last0 (@nil val))) (@cons val last (@nil val))) (@app val (@app val prefix (@cons val last0 (@nil val))) (@cons val last (@nil val))))) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@lseg CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS Ews (@app val prefix (@cons val last0 (@nil val))) hd p) (@malloc_token CompSpecs Ews t_struct_elem p)) (@data_at CompSpecs Ews t_struct_elem (@pair val val last nullval) p)))) *)
    entailer.
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (tc_environ Delta)) (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _p p) (@cons localdef (temp _n (Vint (Int.repr (@sizeof (@cenv_cs CompSpecs) t)))) (@cons localdef (gvars gv) (@nil localdef)))) (SEPx (@cons mpred (mem_mgr gv) (@cons mpred (if @eq_dec val Memory.EqDec_val p nullval then @emp mpred Nveric Sveric else @sepcon mpred Nveric Sveric (@malloc_token CompSpecs Ews t p) (@data_at_ CompSpecs Ews t p)) (@nil mpred))))))) (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _p p) (@nil localdef)) (SEPx (@cons mpred (mem_mgr gv) (@cons mpred (@sepcon mpred Nveric Sveric (@malloc_token CompSpecs Ews t p) (@data_at_ CompSpecs Ews t p)) (@nil mpred)))))) *)
 destruct hd; try contradiction.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (mem_mgr gv) (@malloc_token CompSpecs Ews t_struct_elem p)) (@data_at CompSpecs Ews t_struct_elem (@pair val val (Vint i) Vundef) p)) (@andp mpred Nveric (@prop mpred Nveric (@eq val p p)) (@sepcon mpred Nveric Sveric (mem_mgr gv) (@sepcon mpred Nveric Sveric (@malloc_token CompSpecs Ews t_struct_elem p) (@data_at CompSpecs Ews t_struct_elem (@pair val val (Vint i) Vundef) p)))) *)
 entailer!.
Qed.

Lemma body_fifo_new: semax_body Vprog Gprog f_fifo_new fifo_new_spec.
Proof.
(* Goal: semax_body Vprog Gprog CompSpecs f_make_elem make_elem_spec *)
  start_function.

  forward_call (* Q = surely_malloc(sizeof ( *Q)); *)
     (t_struct_fifo, gv).
(* Goal: and (and (Z.le Z0 (@sizeof (@cenv_cs CompSpecs) t_struct_elem)) (Z.le (@sizeof (@cenv_cs CompSpecs) t_struct_elem) Int.max_unsigned)) (and (@eq bool (@complete_legal_cosu_type (@cenv_cs CompSpecs) t_struct_elem) true) (@eq bool (@natural_aligned CompSpecs natural_alignment t_struct_elem) true)) *)
(* Goal: semax CompSpecs Espec Delta (@exp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) val (fun vret : val => PROPx (@nil Prop) (LOCALx (@cons localdef (temp _p vret) (@cons localdef (temp _data (Vint i)) (@cons localdef (gvars gv) (@nil localdef)))) (SEPx (@cons mpred (mem_mgr gv) (@cons mpred (@sepcon mpred Nveric Sveric (@malloc_token CompSpecs Ews t_struct_elem vret) (@data_at_ CompSpecs Ews t_struct_elem vret)) (@nil mpred))))))) (Ssequence (Sassign (Efield (Ederef (Etempvar _p (tptr (Tstruct _elem noattr))) (Tstruct _elem noattr)) _data tint) (Etempvar _data tint)) MORE_COMMANDS) POSTCONDITION *)
    split3; simpl; auto; computable.
(* Goal: semax CompSpecs Espec Delta (@exp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) val (fun vret : val => PROPx (@nil Prop) (LOCALx (@cons localdef (temp _Q vret) (@cons localdef (gvars gv) (@nil localdef))) (SEPx (@cons mpred (mem_mgr gv) (@cons mpred (@sepcon mpred Nveric Sveric (@malloc_token CompSpecs Ews t_struct_fifo vret) (@data_at_ CompSpecs Ews t_struct_fifo vret)) (@nil mpred))))))) (Ssequence (Sassign (Efield (Ederef (Etempvar _Q (tptr (Tstruct _fifo noattr))) (Tstruct _fifo noattr)) _head (tptr (Tstruct _elem noattr))) (Ecast (Econst_int (Int.repr Z0) tint) (tptr tvoid))) MORE_COMMANDS) POSTCONDITION *)
  Intros q.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _Q q) (@cons localdef (gvars gv) (@nil localdef))) (SEPx (@cons mpred (mem_mgr gv) (@cons mpred (@malloc_token CompSpecs Ews t_struct_fifo q) (@cons mpred (@data_at_ CompSpecs Ews t_struct_fifo q) (@nil mpred))))))) (Ssequence (Sassign (Efield (Ederef (Etempvar _Q (tptr (Tstruct _fifo noattr))) (Tstruct _fifo noattr)) _head (tptr (Tstruct _elem noattr))) (Ecast (Econst_int (Int.repr Z0) tint) (tptr tvoid))) MORE_COMMANDS) POSTCONDITION *)
  assert_PROP (field_compatible t_struct_fifo [] q).
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (mem_mgr gv) (@malloc_token CompSpecs Ews t_struct_elem p)) (@data_at CompSpecs Ews t_struct_elem (@pair val val (Vint i) Vundef) p)) (@andp mpred Nveric (@prop mpred Nveric (@eq val p p)) (@sepcon mpred Nveric Sveric (mem_mgr gv) (@sepcon mpred Nveric Sveric (@malloc_token CompSpecs Ews t_struct_elem p) (@data_at CompSpecs Ews t_struct_elem (@pair val val (Vint i) Vundef) p)))) *)
   entailer!.
  forward. (* Q->head = NULL; *)
  forward. (* Q->tail = NULL; *)
  forward. (* return Q; *)
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Ews t_struct_fifo (@pair val val x tl) q) (@malloc_token CompSpecs Ews t_struct_fifo q)) (@malloc_token CompSpecs Ews t_struct_elem hd)) (@list_cell CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS Ews v hd)) (@field_at CompSpecs Ews (@list_struct CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS) (@cons gfield (StructField _next) (@nil gfield)) x hd)) (@lseg CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS Ews prefix x tl)) (@malloc_token CompSpecs Ews t_struct_elem tl)) (@data_at CompSpecs Ews t_struct_elem (@pair val val last nullval) tl)) (@andp mpred Nveric (@prop mpred Nveric (@eq val hd hd)) (@sepcon mpred Nveric Sveric (fifo (@app val prefix (@cons val last (@nil val))) q) (@sepcon mpred Nveric Sveric (@malloc_token CompSpecs Ews t_struct_elem hd) (@data_at CompSpecs Ews t_struct_elem (@pair val val v Vundef) hd)))) *)
  Exists q. unfold fifo, fifo_body. Exists (nullval,nullval).
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (mem_mgr gv) (@malloc_token CompSpecs Ews t_struct_fifo q)) (@data_at CompSpecs Ews t_struct_fifo (@pair val val (Vint (Int.repr Z0)) (Vint (Int.repr Z0))) q)) (@andp mpred Nveric (@prop mpred Nveric (@eq val q q)) (@sepcon mpred Nveric Sveric (mem_mgr gv) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@andp mpred Nveric (@andp mpred Nveric (@prop mpred Nveric (is_pointer_or_null nullval)) (@prop mpred Nveric (is_pointer_or_null nullval))) (@data_at CompSpecs Ews t_struct_fifo (@pair val val nullval nullval) q)) (@malloc_token CompSpecs Ews t_struct_fifo q)) (if @isnil val (@nil val) then @andp mpred Nveric (@prop mpred Nveric (@eq val nullval nullval)) (@emp mpred Nveric Sveric) else @exp mpred Nveric (list val) (fun prefix : list val => @exp mpred Nveric val (fun last : val => @andp mpred Nveric (@prop mpred Nveric (@eq (list val) (@nil val) (@app val prefix (@cons val last (@nil val))))) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@lseg CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS Ews prefix nullval nullval) (@malloc_token CompSpecs Ews t_struct_elem nullval)) (@data_at CompSpecs Ews t_struct_elem (@pair val val last nullval) nullval)))))))) *)
  rewrite if_true by auto.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@list_cell CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS Ews v hd) (@field_at CompSpecs Ews (@list_struct CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS) (@cons gfield (StructField _next) (@nil gfield)) x hd)) (@sepcon mpred Nveric Sveric (@list_cell CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS Ews v hd) (@field_at CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) Vundef hd)) *)
  simpl sizeof.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (mem_mgr gv) (@malloc_token CompSpecs Ews t_struct_elem p)) (@data_at CompSpecs Ews t_struct_elem (@pair val val (Vint i) Vundef) p)) (@andp mpred Nveric (@prop mpred Nveric (@eq val p p)) (@sepcon mpred Nveric Sveric (mem_mgr gv) (@sepcon mpred Nveric Sveric (@malloc_token CompSpecs Ews t_struct_elem p) (@data_at CompSpecs Ews t_struct_elem (@pair val val (Vint i) Vundef) p)))) *)
  entailer!.
Qed.

Lemma body_fifo_put: semax_body Vprog Gprog f_fifo_put fifo_put_spec.
Proof.
(* Goal: semax_body Vprog Gprog CompSpecs f_make_elem make_elem_spec *)
start_function.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _Q q) (@cons localdef (temp _p p) (@nil localdef))) (SEPx (@cons mpred (fifo contents q) (@cons mpred (@malloc_token CompSpecs Ews t_struct_elem p) (@cons mpred (@data_at CompSpecs Ews t_struct_elem (@pair val val last Vundef) p) (@nil mpred))))))) (Ssequence (Ssequence (Sassign (Efield (Ederef (Etempvar _p (tptr (Tstruct _elem noattr))) (Tstruct _elem noattr)) _next (tptr (Tstruct _elem noattr))) (Ecast (Econst_int (Int.repr Z0) tint) (tptr tvoid))) (Ssequence (Sset _h (Efield (Ederef (Etempvar _Q (tptr (Tstruct _fifo noattr))) (Tstruct _fifo noattr)) _head (tptr (Tstruct _elem noattr)))) (Sifthenelse (Ebinop Oeq (Etempvar _h (tptr (Tstruct _elem noattr))) (Ecast (Econst_int (Int.repr Z0) tint) (tptr tvoid)) tint) (Ssequence (Sassign (Efield (Ederef (Etempvar _Q (tptr (Tstruct _fifo noattr))) (Tstruct _fifo noattr)) _head (tptr (Tstruct _elem noattr))) (Etempvar _p (tptr (Tstruct _elem noattr)))) (Sassign (Efield (Ederef (Etempvar _Q (tptr (Tstruct _fifo noattr))) (Tstruct _fifo noattr)) _tail (tptr (Tstruct _elem noattr))) (Etempvar _p (tptr (Tstruct _elem noattr))))) (Ssequence (Sset _t (Efield (Ederef (Etempvar _Q (tptr (Tstruct _fifo noattr))) (Tstruct _fifo noattr)) _tail (tptr (Tstruct _elem noattr)))) (Ssequence (Sassign (Efield (Ederef (Etempvar _t (tptr (Tstruct _elem noattr))) (Tstruct _elem noattr)) _next (tptr (Tstruct _elem noattr))) (Etempvar _p (tptr (Tstruct _elem noattr)))) (Sassign (Efield (Ederef (Etempvar _Q (tptr (Tstruct _fifo noattr))) (Tstruct _fifo noattr)) _tail (tptr (Tstruct _elem noattr))) (Etempvar _p (tptr (Tstruct _elem noattr))))))))) MORE_COMMANDS) POSTCONDITION *)
unfold fifo at 1.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _Q q) (@nil localdef)) (SEPx (@cons mpred (@exp mpred Nveric (prod val val) (fun ht : prod val val => let (hd, tl) := ht in @sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@andp mpred Nveric (@andp mpred Nveric (@prop mpred Nveric (is_pointer_or_null hd)) (@prop mpred Nveric (is_pointer_or_null tl))) (@data_at CompSpecs Ews t_struct_fifo (@pair val val hd tl) q)) (@malloc_token CompSpecs Ews t_struct_fifo q)) (if @isnil val (@cons val first contents) then @andp mpred Nveric (@prop mpred Nveric (@eq val hd nullval)) (@emp mpred Nveric Sveric) else @exp mpred Nveric (list val) (fun prefix : list val => @exp mpred Nveric val (fun last : val => @andp mpred Nveric (@prop mpred Nveric (@eq (list val) (@cons val first contents) (@app val prefix (@cons val last (@nil val))))) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@lseg CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS Ews prefix hd tl) (@malloc_token CompSpecs Ews t_struct_elem tl)) (@data_at CompSpecs Ews t_struct_elem (@pair val val last nullval) tl))))))) (@nil mpred))))) (Ssequence (Sset _h (Efield (Ederef (Etempvar _Q (tptr (Tstruct _fifo noattr))) (Tstruct _fifo noattr)) _head (tptr (Tstruct _elem noattr)))) MORE_COMMANDS) POSTCONDITION *)
Intros ht; destruct ht as [hd tl].
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _h hd) (@cons localdef (temp _Q q) (@nil localdef))) (SEPx (@cons mpred (@data_at CompSpecs Ews t_struct_fifo (@pair val val hd tl) q) (@cons mpred (@malloc_token CompSpecs Ews t_struct_fifo q) (@cons mpred (@andp mpred Nveric (@prop mpred Nveric (ptr_eq hd tl)) (@emp mpred Nveric Sveric)) (@cons mpred (@malloc_token CompSpecs Ews t_struct_elem tl) (@cons mpred (@data_at CompSpecs Ews t_struct_elem (@pair val val last nullval) tl) (@nil mpred))))))))) (Ssequence (Sset _n (Efield (Ederef (Etempvar _h (tptr (Tstruct _elem noattr))) (Tstruct _elem noattr)) _next (tptr (Tstruct _elem noattr)))) MORE_COMMANDS) POSTCONDITION *)
Intros.
forward. (* p->next = NULL; *)
forward. (*   h = Q->head; *)
forward_if
  (PROP() LOCAL () SEP (fifo (contents ++ last :: nil) q))%assert.
* unfold fifo_body; if_tac; entailer.  (* typechecking clause *) 
      (* TODO: In the line above, entailer works but not entailer! *)
* (* then clause *)
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Ews t_struct_fifo (@pair val val p p) q) (@malloc_token CompSpecs Ews t_struct_fifo q)) (@andp mpred Nveric (@prop mpred Nveric (@eq val nullval nullval)) (@emp mpred Nveric Sveric))) (@malloc_token CompSpecs Ews t_struct_elem p)) (@data_at CompSpecs Ews t_struct_elem (@pair val val last (Vint (Int.repr Z0))) p)) (@exp mpred Nveric (prod val val) (fun ht : prod val val => let (hd, tl) := ht in @sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@andp mpred Nveric (@andp mpred Nveric (@prop mpred Nveric (is_pointer_or_null hd)) (@prop mpred Nveric (is_pointer_or_null tl))) (@data_at CompSpecs Ews t_struct_fifo (@pair val val hd tl) q)) (@malloc_token CompSpecs Ews t_struct_fifo q)) (if @isnil val (@app val contents (@cons val last (@nil val))) then @andp mpred Nveric (@prop mpred Nveric (@eq val hd nullval)) (@emp mpred Nveric Sveric) else @exp mpred Nveric (list val) (fun prefix : list val => @exp mpred Nveric val (fun last0 : val => @andp mpred Nveric (@prop mpred Nveric (@eq (list val) (@app val contents (@cons val last (@nil val))) (@app val prefix (@cons val last0 (@nil val))))) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@lseg CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS Ews prefix hd tl) (@malloc_token CompSpecs Ews t_struct_elem tl)) (@data_at CompSpecs Ews t_struct_elem (@pair val val last0 nullval) tl))))))) *)
  subst.
  forward. (* Q->head=p; *)
  forward. (* Q->tail=p; *)
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Ews t_struct_fifo (@pair val val hd p) q) (@malloc_token CompSpecs Ews t_struct_fifo q)) (@lseg CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS Ews prefix hd tl)) (@malloc_token CompSpecs Ews t_struct_elem tl)) (@data_at CompSpecs Ews t_struct_elem (@pair val val last0 p) tl)) (@malloc_token CompSpecs Ews t_struct_elem p)) (@data_at CompSpecs Ews t_struct_elem (@pair val val last (Vint (Int.repr Z0))) p)) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@andp mpred Nveric (@andp mpred Nveric (@prop mpred Nveric (is_pointer_or_null hd)) (@prop mpred Nveric (is_pointer_or_null p))) (@data_at CompSpecs Ews t_struct_fifo (@pair val val hd p) q)) (@malloc_token CompSpecs Ews t_struct_fifo q)) (@andp mpred Nveric (@prop mpred Nveric (@eq (list val) (@app val (@app val prefix (@cons val last0 (@nil val))) (@cons val last (@nil val))) (@app val (@app val prefix (@cons val last0 (@nil val))) (@cons val last (@nil val))))) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@lseg CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS Ews (@app val prefix (@cons val last0 (@nil val))) hd p) (@malloc_token CompSpecs Ews t_struct_elem p)) (@data_at CompSpecs Ews t_struct_elem (@pair val val last nullval) p)))) *)
  entailer.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Ews t_struct_fifo (@pair val val x tl) q) (@malloc_token CompSpecs Ews t_struct_fifo q)) (@malloc_token CompSpecs Ews t_struct_elem hd)) (@list_cell CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS Ews v hd)) (@field_at CompSpecs Ews (@list_struct CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS) (@cons gfield (StructField _next) (@nil gfield)) x hd)) (@lseg CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS Ews prefix x tl)) (@malloc_token CompSpecs Ews t_struct_elem tl)) (@data_at CompSpecs Ews t_struct_elem (@pair val val last nullval) tl)) (@andp mpred Nveric (@prop mpred Nveric (@eq val hd hd)) (@sepcon mpred Nveric Sveric (fifo (@app val prefix (@cons val last (@nil val))) q) (@sepcon mpred Nveric Sveric (@malloc_token CompSpecs Ews t_struct_elem hd) (@data_at CompSpecs Ews t_struct_elem (@pair val val v Vundef) hd)))) *)
  unfold fifo, fifo_body.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _t tl) (@cons localdef (temp _h hd) (@cons localdef (temp _Q q) (@cons localdef (temp _p p) (@nil localdef))))) (SEPx (@cons mpred (@data_at CompSpecs Ews t_struct_fifo (@pair val val hd tl) q) (@cons mpred (@malloc_token CompSpecs Ews t_struct_fifo q) (@cons mpred (if @isnil val contents then @andp mpred Nveric (@prop mpred Nveric (@eq val hd nullval)) (@emp mpred Nveric Sveric) else @exp mpred Nveric (list val) (fun prefix : list val => @exp mpred Nveric val (fun last : val => @andp mpred Nveric (@prop mpred Nveric (@eq (list val) contents (@app val prefix (@cons val last (@nil val))))) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@lseg CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS Ews prefix hd tl) (@malloc_token CompSpecs Ews t_struct_elem tl)) (@data_at CompSpecs Ews t_struct_elem (@pair val val last nullval) tl))))) (@cons mpred (@malloc_token CompSpecs Ews t_struct_elem p) (@cons mpred (@data_at CompSpecs Ews t_struct_elem (@pair val val last (Vint (Int.repr Z0))) p) (@nil mpred))))))))) (Ssequence (Sassign (Efield (Ederef (Etempvar _t (tptr (Tstruct _elem noattr))) (Tstruct _elem noattr)) _next (tptr (Tstruct _elem noattr))) (Etempvar _p (tptr (Tstruct _elem noattr)))) MORE_COMMANDS) POSTCONDITION *)
  destruct (isnil contents).
  + subst. Exists (p,p).
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (tc_environ Delta)) (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _p nullval) (@cons localdef (temp _n (Vint (Int.repr (@sizeof (@cenv_cs CompSpecs) t)))) (@cons localdef (gvars gv) (@nil localdef)))) (SEPx (@cons mpred (mem_mgr gv) (@cons mpred (@emp mpred Nveric Sveric) (@nil mpred))))))) (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _p nullval) (@nil localdef)) (SEPx (@cons mpred (mem_mgr gv) (@cons mpred (@sepcon mpred Nveric Sveric (@malloc_token CompSpecs Ews t nullval) (@data_at_ CompSpecs Ews t nullval)) (@nil mpred)))))) *)
     simpl. rewrite if_false by congruence.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Ews t_struct_fifo (@pair val val p p) q) (@malloc_token CompSpecs Ews t_struct_fifo q)) (@andp mpred Nveric (@prop mpred Nveric (@eq val nullval nullval)) (@emp mpred Nveric Sveric))) (@malloc_token CompSpecs Ews t_struct_elem p)) (@data_at CompSpecs Ews t_struct_elem (@pair val val last (Vint (Int.repr Z0))) p)) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@andp mpred Nveric (@andp mpred Nveric (@prop mpred Nveric (is_pointer_or_null p)) (@prop mpred Nveric (is_pointer_or_null p))) (@data_at CompSpecs Ews t_struct_fifo (@pair val val p p) q)) (@malloc_token CompSpecs Ews t_struct_fifo q)) (@exp mpred Nveric (list val) (fun prefix : list val => @exp mpred Nveric val (fun last0 : val => @andp mpred Nveric (@prop mpred Nveric (@eq (list val) (@cons val last (@nil val)) (@app val prefix (@cons val last0 (@nil val))))) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@lseg CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS Ews prefix p p) (@malloc_token CompSpecs Ews t_struct_elem p)) (@data_at CompSpecs Ews t_struct_elem (@pair val val last0 nullval) p)))))) *)
     Exists (@nil val) last.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _h hd) (@cons localdef (temp _Q q) (@nil localdef))) (SEPx (@cons mpred (@data_at CompSpecs Ews t_struct_fifo (@pair val val hd tl) q) (@cons mpred (@malloc_token CompSpecs Ews t_struct_fifo q) (@cons mpred (@lseg CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS Ews (@nil val) hd tl) (@cons mpred (@malloc_token CompSpecs Ews t_struct_elem tl) (@cons mpred (@data_at CompSpecs Ews t_struct_elem (@pair val val last nullval) tl) (@nil mpred))))))))) (Ssequence (Sset _n (Efield (Ederef (Etempvar _h (tptr (Tstruct _elem noattr))) (Tstruct _elem noattr)) _next (tptr (Tstruct _elem noattr)))) MORE_COMMANDS) POSTCONDITION *)
      rewrite @lseg_nil_eq by auto.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (mem_mgr gv) (@malloc_token CompSpecs Ews t_struct_elem p)) (@data_at CompSpecs Ews t_struct_elem (@pair val val (Vint i) Vundef) p)) (@andp mpred Nveric (@prop mpred Nveric (@eq val p p)) (@sepcon mpred Nveric Sveric (mem_mgr gv) (@sepcon mpred Nveric Sveric (@malloc_token CompSpecs Ews t_struct_elem p) (@data_at CompSpecs Ews t_struct_elem (@pair val val (Vint i) Vundef) p)))) *)
      entailer!.
   + Intros prefix last0.
      destruct prefix;
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (mem_mgr gv) (@malloc_token CompSpecs Ews t_struct_elem p)) (@data_at CompSpecs Ews t_struct_elem (@pair val val (Vint i) Vundef) p)) (@andp mpred Nveric (@prop mpred Nveric (@eq val p p)) (@sepcon mpred Nveric Sveric (mem_mgr gv) (@sepcon mpred Nveric Sveric (@malloc_token CompSpecs Ews t_struct_elem p) (@data_at CompSpecs Ews t_struct_elem (@pair val val (Vint i) Vundef) p)))) *)
      entailer!.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _h hd) (@cons localdef (temp _Q q) (@nil localdef))) (SEPx (@cons mpred (@data_at CompSpecs Ews t_struct_fifo (@pair val val hd tl) q) (@cons mpred (@malloc_token CompSpecs Ews t_struct_fifo q) (@cons mpred (@lseg CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS Ews (@cons val v prefix) hd tl) (@cons mpred (@malloc_token CompSpecs Ews t_struct_elem tl) (@cons mpred (@data_at CompSpecs Ews t_struct_elem (@pair val val last nullval) tl) (@nil mpred))))))))) (Ssequence (Sset _n (Efield (Ederef (Etempvar _h (tptr (Tstruct _elem noattr))) (Tstruct _elem noattr)) _next (tptr (Tstruct _elem noattr)))) MORE_COMMANDS) POSTCONDITION *)
      rewrite @lseg_cons_eq by auto. 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 (@sepcon mpred Nveric Sveric (@data_at CompSpecs Ews t_struct_fifo (@pair val val p p) q) (@malloc_token CompSpecs Ews t_struct_fifo q)) (@andp mpred Nveric (@prop mpred Nveric (not match tl with | Vundef => False | Vint n2 => and (@eq bool Archi.ptr64 false) (and (@eq bool (Int.eq Int.zero n2) true) (@eq bool (Int.eq Int.zero (Int.repr Z0)) true)) | Vlong i => False | Vfloat f => False | Vsingle f => False | Vptr b i => False end)) (@exp mpred Nveric val (fun y : val => @sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@andp mpred Nveric (@prop mpred Nveric (is_pointer_or_null y)) (@malloc_token CompSpecs Ews t_struct_elem nullval)) (@list_cell CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS Ews v nullval)) (@field_at CompSpecs Ews (@list_struct CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS) (@cons gfield (StructField _next) (@nil gfield)) y nullval)) (@lseg CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS Ews prefix y tl))))) (@malloc_token CompSpecs Ews t_struct_elem tl)) (@data_at CompSpecs Ews t_struct_elem (@pair val val last0 nullval) tl)) (@malloc_token CompSpecs Ews t_struct_elem p)) (@data_at CompSpecs Ews t_struct_elem (@pair val val last (Vint (Int.repr Z0))) p)) (@exp mpred Nveric (prod val val) (fun ht : prod val val => let (hd, tl) := ht in @sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@andp mpred Nveric (@andp mpred Nveric (@prop mpred Nveric (is_pointer_or_null hd)) (@prop mpred Nveric (is_pointer_or_null tl))) (@data_at CompSpecs Ews t_struct_fifo (@pair val val hd tl) q)) (@malloc_token CompSpecs Ews t_struct_fifo q)) (if @isnil val (@cons val v (@app val (@app val prefix (@cons val last0 (@nil val))) (@cons val last (@nil val)))) then @andp mpred Nveric (@prop mpred Nveric (@eq val hd nullval)) (@emp mpred Nveric Sveric) else @exp mpred Nveric (list val) (fun prefix0 : list val => @exp mpred Nveric val (fun last1 : val => @andp mpred Nveric (@prop mpred Nveric (@eq (list val) (@cons val v (@app val (@app val prefix (@cons val last0 (@nil val))) (@cons val last (@nil val)))) (@app val prefix0 (@cons val last1 (@nil val))))) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@lseg CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS Ews prefix0 hd tl) (@malloc_token CompSpecs Ews t_struct_elem tl)) (@data_at CompSpecs Ews t_struct_elem (@pair val val last1 nullval) tl))))))) *)
      Intros y.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (mem_mgr gv) (@malloc_token CompSpecs Ews t_struct_elem p)) (@data_at CompSpecs Ews t_struct_elem (@pair val val (Vint i) Vundef) p)) (@andp mpred Nveric (@prop mpred Nveric (@eq val p p)) (@sepcon mpred Nveric Sveric (mem_mgr gv) (@sepcon mpred Nveric Sveric (@malloc_token CompSpecs Ews t_struct_elem p) (@data_at CompSpecs Ews t_struct_elem (@pair val val (Vint i) Vundef) p)))) *)
      entailer!.
* (* else clause *)
  forward. (*  t = Q->tail; *)
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _t tl) (@cons localdef (temp _h hd) (@cons localdef (temp _Q q) (@cons localdef (temp _p p) (@nil localdef))))) (SEPx (@cons mpred (@data_at CompSpecs Ews t_struct_fifo (@pair val val hd tl) q) (@cons mpred (@malloc_token CompSpecs Ews t_struct_fifo q) (@cons mpred (fifo_body contents hd tl) (@cons mpred (@malloc_token CompSpecs Ews t_struct_elem p) (@cons mpred (@data_at CompSpecs Ews t_struct_elem (@pair val val last (Vint (Int.repr Z0))) p) (@nil mpred))))))))) (Ssequence (Sassign (Efield (Ederef (Etempvar _t (tptr (Tstruct _elem noattr))) (Tstruct _elem noattr)) _next (tptr (Tstruct _elem noattr))) (Etempvar _p (tptr (Tstruct _elem noattr)))) MORE_COMMANDS) POSTCONDITION *)
  unfold fifo_body.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _t tl) (@cons localdef (temp _h hd) (@cons localdef (temp _Q q) (@cons localdef (temp _p p) (@nil localdef))))) (SEPx (@cons mpred (@data_at CompSpecs Ews t_struct_fifo (@pair val val hd tl) q) (@cons mpred (@malloc_token CompSpecs Ews t_struct_fifo q) (@cons mpred (if @isnil val contents then @andp mpred Nveric (@prop mpred Nveric (@eq val hd nullval)) (@emp mpred Nveric Sveric) else @exp mpred Nveric (list val) (fun prefix : list val => @exp mpred Nveric val (fun last : val => @andp mpred Nveric (@prop mpred Nveric (@eq (list val) contents (@app val prefix (@cons val last (@nil val))))) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@lseg CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS Ews prefix hd tl) (@malloc_token CompSpecs Ews t_struct_elem tl)) (@data_at CompSpecs Ews t_struct_elem (@pair val val last nullval) tl))))) (@cons mpred (@malloc_token CompSpecs Ews t_struct_elem p) (@cons mpred (@data_at CompSpecs Ews t_struct_elem (@pair val val last (Vint (Int.repr Z0))) p) (@nil mpred))))))))) (Ssequence (Sassign (Efield (Ederef (Etempvar _t (tptr (Tstruct _elem noattr))) (Tstruct _elem noattr)) _next (tptr (Tstruct _elem noattr))) (Etempvar _p (tptr (Tstruct _elem noattr)))) MORE_COMMANDS) POSTCONDITION *)
  destruct (isnil contents).
  + Intros. contradiction H; auto.
  + Intros prefix last0.
     forward. (*  t->next=p; *)
     forward. (* Q->tail=p; *)
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (mem_mgr gv) (@malloc_token CompSpecs Ews t_struct_elem p)) (@data_at CompSpecs Ews t_struct_elem (@pair val val (Vint i) Vundef) p)) (@andp mpred Nveric (@prop mpred Nveric (@eq val p p)) (@sepcon mpred Nveric Sveric (mem_mgr gv) (@sepcon mpred Nveric Sveric (@malloc_token CompSpecs Ews t_struct_elem p) (@data_at CompSpecs Ews t_struct_elem (@pair val val (Vint i) Vundef) p)))) *)
     entailer!.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Ews t_struct_fifo (@pair val val x tl) q) (@malloc_token CompSpecs Ews t_struct_fifo q)) (@malloc_token CompSpecs Ews t_struct_elem hd)) (@list_cell CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS Ews v hd)) (@field_at CompSpecs Ews (@list_struct CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS) (@cons gfield (StructField _next) (@nil gfield)) x hd)) (@lseg CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS Ews prefix x tl)) (@malloc_token CompSpecs Ews t_struct_elem tl)) (@data_at CompSpecs Ews t_struct_elem (@pair val val last nullval) tl)) (@andp mpred Nveric (@prop mpred Nveric (@eq val hd hd)) (@sepcon mpred Nveric Sveric (fifo (@app val prefix (@cons val last (@nil val))) q) (@sepcon mpred Nveric Sveric (@malloc_token CompSpecs Ews t_struct_elem hd) (@data_at CompSpecs Ews t_struct_elem (@pair val val v Vundef) hd)))) *)
     unfold fifo, fifo_body. Exists (hd, p).
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Ews t_struct_fifo (@pair val val hd p) q) (@malloc_token CompSpecs Ews t_struct_fifo q)) (@lseg CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS Ews prefix hd tl)) (@malloc_token CompSpecs Ews t_struct_elem tl)) (@data_at CompSpecs Ews t_struct_elem (@pair val val last0 p) tl)) (@malloc_token CompSpecs Ews t_struct_elem p)) (@data_at CompSpecs Ews t_struct_elem (@pair val val last (Vint (Int.repr Z0))) p)) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@andp mpred Nveric (@andp mpred Nveric (@prop mpred Nveric (is_pointer_or_null hd)) (@prop mpred Nveric (is_pointer_or_null p))) (@data_at CompSpecs Ews t_struct_fifo (@pair val val hd p) q)) (@malloc_token CompSpecs Ews t_struct_fifo q)) (if @isnil val (@app val (@app val prefix (@cons val last0 (@nil val))) (@cons val last (@nil val))) then @andp mpred Nveric (@prop mpred Nveric (@eq val hd nullval)) (@emp mpred Nveric Sveric) else @exp mpred Nveric (list val) (fun prefix0 : list val => @exp mpred Nveric val (fun last1 : val => @andp mpred Nveric (@prop mpred Nveric (@eq (list val) (@app val (@app val prefix (@cons val last0 (@nil val))) (@cons val last (@nil val))) (@app val prefix0 (@cons val last1 (@nil val))))) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@lseg CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS Ews prefix0 hd p) (@malloc_token CompSpecs Ews t_struct_elem p)) (@data_at CompSpecs Ews t_struct_elem (@pair val val last1 nullval) p)))))) *)
     rewrite if_false by (clear; destruct prefix; simpl; congruence).
     Exists  (prefix ++ last0 :: nil) last.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Ews t_struct_fifo (@pair val val hd p) q) (@malloc_token CompSpecs Ews t_struct_fifo q)) (@lseg CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS Ews prefix hd tl)) (@malloc_token CompSpecs Ews t_struct_elem tl)) (@data_at CompSpecs Ews t_struct_elem (@pair val val last0 p) tl)) (@malloc_token CompSpecs Ews t_struct_elem p)) (@data_at CompSpecs Ews t_struct_elem (@pair val val last (Vint (Int.repr Z0))) p)) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@andp mpred Nveric (@andp mpred Nveric (@prop mpred Nveric (is_pointer_or_null hd)) (@prop mpred Nveric (is_pointer_or_null p))) (@data_at CompSpecs Ews t_struct_fifo (@pair val val hd p) q)) (@malloc_token CompSpecs Ews t_struct_fifo q)) (@andp mpred Nveric (@prop mpred Nveric (@eq (list val) (@app val (@app val prefix (@cons val last0 (@nil val))) (@cons val last (@nil val))) (@app val (@app val prefix (@cons val last0 (@nil val))) (@cons val last (@nil val))))) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@lseg CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS Ews (@app val prefix (@cons val last0 (@nil val))) hd p) (@malloc_token CompSpecs Ews t_struct_elem p)) (@data_at CompSpecs Ews t_struct_elem (@pair val val last nullval) p)))) *)
     entailer.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Ews t_struct_fifo (@pair val val hd p) q) (@malloc_token CompSpecs Ews t_struct_fifo q)) (@lseg CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS Ews prefix hd tl)) (@malloc_token CompSpecs Ews t_struct_elem tl)) (@data_at CompSpecs Ews t_struct_elem (@pair val val last0 p) tl)) (@malloc_token CompSpecs Ews t_struct_elem p)) (@data_at CompSpecs Ews t_struct_elem (@pair val val last (Vint (Int.repr Z0))) p)) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Ews t_struct_fifo (@pair val val hd p) q) (@malloc_token CompSpecs Ews t_struct_fifo q)) (@lseg CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS Ews (@app val prefix (@cons val last0 (@nil val))) hd p)) (@malloc_token CompSpecs Ews t_struct_elem p)) (@data_at CompSpecs Ews t_struct_elem (@pair val val last nullval) p)) *)
     rewrite (field_at_list_cell Ews last0 p).
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Ews t_struct_fifo (@pair val val hd p) q) (@malloc_token CompSpecs Ews t_struct_fifo q)) (@lseg CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS Ews prefix hd tl)) (@malloc_token CompSpecs Ews t_struct_elem tl)) (@sepcon mpred Nveric Sveric (@list_cell CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS Ews last0 tl) (@field_at CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) p tl))) (@malloc_token CompSpecs Ews t_struct_elem p)) (@data_at CompSpecs Ews t_struct_elem (@pair val val last (Vint (Int.repr Z0))) p)) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Ews t_struct_fifo (@pair val val hd p) q) (@malloc_token CompSpecs Ews t_struct_fifo q)) (@lseg CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS Ews (@app val prefix (@cons val last0 (@nil val))) hd p)) (@malloc_token CompSpecs Ews t_struct_elem p)) (@data_at CompSpecs Ews t_struct_elem (@pair val val last nullval) p)) *)
     unfold_data_at (@data_at CompSpecs Ews t_struct_elem (last,nullval) p).
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Ews t_struct_fifo (@pair val val hd p) q) (@malloc_token CompSpecs Ews t_struct_fifo q)) (@lseg CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS Ews prefix hd tl)) (@malloc_token CompSpecs Ews t_struct_elem tl)) (@sepcon mpred Nveric Sveric (@list_cell CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS Ews last0 tl) (@field_at CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) p tl))) (@malloc_token CompSpecs Ews t_struct_elem p)) (@data_at CompSpecs Ews t_struct_elem (@pair val val last (Vint (Int.repr Z0))) p)) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Ews t_struct_fifo (@pair val val hd p) q) (@malloc_token CompSpecs Ews t_struct_fifo q)) (@lseg CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS Ews (@app val prefix (@cons val last0 (@nil val))) hd p)) (@malloc_token CompSpecs Ews t_struct_elem p)) (@sepcon mpred Nveric Sveric (@field_at CompSpecs Ews t_struct_elem (@cons gfield (StructField _data) (@nil gfield)) last p) (@field_at CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) nullval p))) *)
     unfold_data_at (data_at _ _ _ p).
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@list_cell CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS Ews v hd) (@field_at CompSpecs Ews (@list_struct CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS) (@cons gfield (StructField _next) (@nil gfield)) x hd)) (@sepcon mpred Nveric Sveric (@list_cell CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS Ews v hd) (@field_at CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) Vundef hd)) *)
     simpl sizeof.
     match goal with
     | |- _ |-- _ * _ * (_ * ?AA) => remember AA as A
     end.     (* prevent it from canceling! *)
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@list_cell CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS Ews v hd) (@field_at CompSpecs Ews (@list_struct CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS) (@cons gfield (StructField _next) (@nil gfield)) x hd)) (@sepcon mpred Nveric Sveric (@list_cell CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS Ews v hd) (@field_at CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) Vundef hd)) *)
     cancel. subst A.
     eapply derives_trans;
        [ | apply (lseg_cons_right_neq QS Ews prefix hd last0 tl nullval p ); auto].
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@list_cell CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS Ews v hd) (@field_at CompSpecs Ews (@list_struct CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS) (@cons gfield (StructField _next) (@nil gfield)) x hd)) (@sepcon mpred Nveric Sveric (@list_cell CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS Ews v hd) (@field_at CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) Vundef hd)) *)
     simpl sizeof.  cancel.
* (* after the if *)
     forward. (* return ; *)
Qed.

Lemma body_fifo_get: semax_body Vprog Gprog f_fifo_get fifo_get_spec.
Proof.
(* Goal: semax_body Vprog Gprog CompSpecs f_make_elem make_elem_spec *)
start_function.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _Q q) (@nil localdef)) (SEPx (@cons mpred (fifo (@cons val first contents) q) (@nil mpred))))) (Ssequence (Sset _h (Efield (Ederef (Etempvar _Q (tptr (Tstruct _fifo noattr))) (Tstruct _fifo noattr)) _head (tptr (Tstruct _elem noattr)))) MORE_COMMANDS) POSTCONDITION *)
unfold fifo at 1, fifo_body.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _Q q) (@nil localdef)) (SEPx (@cons mpred (@exp mpred Nveric (prod val val) (fun ht : prod val val => let (hd, tl) := ht in @sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@andp mpred Nveric (@andp mpred Nveric (@prop mpred Nveric (is_pointer_or_null hd)) (@prop mpred Nveric (is_pointer_or_null tl))) (@data_at CompSpecs Ews t_struct_fifo (@pair val val hd tl) q)) (@malloc_token CompSpecs Ews t_struct_fifo q)) (if @isnil val (@cons val first contents) then @andp mpred Nveric (@prop mpred Nveric (@eq val hd nullval)) (@emp mpred Nveric Sveric) else @exp mpred Nveric (list val) (fun prefix : list val => @exp mpred Nveric val (fun last : val => @andp mpred Nveric (@prop mpred Nveric (@eq (list val) (@cons val first contents) (@app val prefix (@cons val last (@nil val))))) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@lseg CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS Ews prefix hd tl) (@malloc_token CompSpecs Ews t_struct_elem tl)) (@data_at CompSpecs Ews t_struct_elem (@pair val val last nullval) tl))))))) (@nil mpred))))) (Ssequence (Sset _h (Efield (Ederef (Etempvar _Q (tptr (Tstruct _fifo noattr))) (Tstruct _fifo noattr)) _head (tptr (Tstruct _elem noattr)))) MORE_COMMANDS) POSTCONDITION *)
Intros ht; destruct ht as [hd tl].
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (tc_environ Delta)) (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _p nullval) (@cons localdef (temp _n (Vint (Int.repr (@sizeof (@cenv_cs CompSpecs) t)))) (@cons localdef (gvars gv) (@nil localdef)))) (SEPx (@cons mpred (mem_mgr gv) (@cons mpred (@emp mpred Nveric Sveric) (@nil mpred))))))) (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _p nullval) (@nil localdef)) (SEPx (@cons mpred (mem_mgr gv) (@cons mpred (@sepcon mpred Nveric Sveric (@malloc_token CompSpecs Ews t nullval) (@data_at_ CompSpecs Ews t nullval)) (@nil mpred)))))) *)
rewrite if_false by congruence.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _Q q) (@nil localdef)) (SEPx (@cons mpred (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@andp mpred Nveric (@andp mpred Nveric (@prop mpred Nveric (is_pointer_or_null hd)) (@prop mpred Nveric (is_pointer_or_null tl))) (@data_at CompSpecs Ews t_struct_fifo (@pair val val hd tl) q)) (@malloc_token CompSpecs Ews t_struct_fifo q)) (@exp mpred Nveric (list val) (fun prefix : list val => @exp mpred Nveric val (fun last : val => @andp mpred Nveric (@prop mpred Nveric (@eq (list val) (@cons val first contents) (@app val prefix (@cons val last (@nil val))))) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@lseg CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS Ews prefix hd tl) (@malloc_token CompSpecs Ews t_struct_elem tl)) (@data_at CompSpecs Ews t_struct_elem (@pair val val last nullval) tl)))))) (@nil mpred))))) (Ssequence (Sset _h (Efield (Ederef (Etempvar _Q (tptr (Tstruct _fifo noattr))) (Tstruct _fifo noattr)) _head (tptr (Tstruct _elem noattr)))) MORE_COMMANDS) POSTCONDITION *)
Intros prefix last.
forward.  (*   h = Q->head; *)
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _h hd) (@cons localdef (temp _Q q) (@nil localdef))) (SEPx (@cons mpred (@data_at CompSpecs Ews t_struct_fifo (@pair val val hd tl) q) (@cons mpred (@malloc_token CompSpecs Ews t_struct_fifo q) (@cons mpred (@lseg CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS Ews prefix hd tl) (@cons mpred (@malloc_token CompSpecs Ews t_struct_elem tl) (@cons mpred (@data_at CompSpecs Ews t_struct_elem (@pair val val last nullval) tl) (@nil mpred))))))))) (Ssequence (Sset _n (Efield (Ederef (Etempvar _h (tptr (Tstruct _elem noattr))) (Tstruct _elem noattr)) _next (tptr (Tstruct _elem noattr)))) MORE_COMMANDS) POSTCONDITION *)
destruct prefix; inversion H; clear H.
+
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _h hd) (@cons localdef (temp _Q q) (@nil localdef))) (SEPx (@cons mpred (@data_at CompSpecs Ews t_struct_fifo (@pair val val hd tl) q) (@cons mpred (@malloc_token CompSpecs Ews t_struct_fifo q) (@cons mpred (@lseg CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS Ews (@nil val) hd tl) (@cons mpred (@malloc_token CompSpecs Ews t_struct_elem tl) (@cons mpred (@data_at CompSpecs Ews t_struct_elem (@pair val val last nullval) tl) (@nil mpred))))))))) (Ssequence (Sset _n (Efield (Ederef (Etempvar _h (tptr (Tstruct _elem noattr))) (Tstruct _elem noattr)) _next (tptr (Tstruct _elem noattr)))) MORE_COMMANDS) POSTCONDITION *)
   rewrite @lseg_nil_eq by auto.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _h hd) (@cons localdef (temp _Q q) (@nil localdef))) (SEPx (@cons mpred (@data_at CompSpecs Ews t_struct_fifo (@pair val val hd tl) q) (@cons mpred (@malloc_token CompSpecs Ews t_struct_fifo q) (@cons mpred (@andp mpred Nveric (@prop mpred Nveric (ptr_eq hd tl)) (@emp mpred Nveric Sveric)) (@cons mpred (@malloc_token CompSpecs Ews t_struct_elem tl) (@cons mpred (@data_at CompSpecs Ews t_struct_elem (@pair val val last nullval) tl) (@nil mpred))))))))) (Ssequence (Sset _n (Efield (Ederef (Etempvar _h (tptr (Tstruct _elem noattr))) (Tstruct _elem noattr)) _next (tptr (Tstruct _elem noattr)))) MORE_COMMANDS) POSTCONDITION *)
   Intros.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _h hd) (@cons localdef (temp _Q q) (@nil localdef))) (SEPx (@cons mpred (@data_at CompSpecs Ews t_struct_fifo (@pair val val hd tl) q) (@cons mpred (@malloc_token CompSpecs Ews t_struct_fifo q) (@cons mpred (@malloc_token CompSpecs Ews t_struct_elem hd) (@cons mpred (@list_cell CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS Ews v hd) (@cons mpred (@field_at CompSpecs Ews (@list_struct CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS) (@cons gfield (StructField _next) (@nil gfield)) x hd) (@cons mpred (@lseg CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS Ews prefix x tl) (@cons mpred (@malloc_token CompSpecs Ews t_struct_elem tl) (@cons mpred (@data_at CompSpecs Ews t_struct_elem (@pair val val last nullval) tl) (@nil mpred)))))))))))) (Ssequence (Sset _n (Efield (Ederef (Etempvar _h (tptr (Tstruct _elem noattr))) (Tstruct _elem noattr)) _next (tptr (Tstruct _elem noattr)))) MORE_COMMANDS) POSTCONDITION *)
   subst_any.
   forward. (*  n=h->next; *)
   forward. (* Q->head=n; *)
   forward. (* return p; *)
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Ews t_struct_fifo (@pair val val x tl) q) (@malloc_token CompSpecs Ews t_struct_fifo q)) (@malloc_token CompSpecs Ews t_struct_elem hd)) (@list_cell CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS Ews v hd)) (@field_at CompSpecs Ews (@list_struct CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS) (@cons gfield (StructField _next) (@nil gfield)) x hd)) (@lseg CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS Ews prefix x tl)) (@malloc_token CompSpecs Ews t_struct_elem tl)) (@data_at CompSpecs Ews t_struct_elem (@pair val val last nullval) tl)) (@andp mpred Nveric (@prop mpred Nveric (@eq val hd hd)) (@sepcon mpred Nveric Sveric (fifo (@app val prefix (@cons val last (@nil val))) q) (@sepcon mpred Nveric Sveric (@malloc_token CompSpecs Ews t_struct_elem hd) (@data_at CompSpecs Ews t_struct_elem (@pair val val v Vundef) hd)))) *)
   unfold fifo, fifo_body. Exists tl (nullval, tl).
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (tc_environ Delta)) (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _p nullval) (@cons localdef (temp _n (Vint (Int.repr (@sizeof (@cenv_cs CompSpecs) t)))) (@cons localdef (gvars gv) (@nil localdef)))) (SEPx (@cons mpred (mem_mgr gv) (@cons mpred (@emp mpred Nveric Sveric) (@nil mpred))))))) (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _p nullval) (@nil localdef)) (SEPx (@cons mpred (mem_mgr gv) (@cons mpred (@sepcon mpred Nveric Sveric (@malloc_token CompSpecs Ews t nullval) (@data_at_ CompSpecs Ews t nullval)) (@nil mpred)))))) *)
   rewrite if_true by congruence.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (mem_mgr gv) (@malloc_token CompSpecs Ews t_struct_elem p)) (@data_at CompSpecs Ews t_struct_elem (@pair val val (Vint i) Vundef) p)) (@andp mpred Nveric (@prop mpred Nveric (@eq val p p)) (@sepcon mpred Nveric Sveric (mem_mgr gv) (@sepcon mpred Nveric Sveric (@malloc_token CompSpecs Ews t_struct_elem p) (@data_at CompSpecs Ews t_struct_elem (@pair val val (Vint i) Vundef) p)))) *)
   entailer!. simpl sizeof.
(* Goal: @eq mpred (@data_at CompSpecs sh t_struct_elem (@pair (let (t, _) := @eq_rect Type ((fun it : prod ident type => (fun _ : type => @sigT Type (fun x : Type => x)) (field_type (@fst ident type it) (co_members (@get_co CompSpecs _elem)))) (@pair ident type _data tint)) (fun A0 : Type => A0) ((fun it : prod ident type => (fix type_func_rec (n : nat) (t : type) {struct n} : (fun _ : type => @sigT Type (fun x : Type => x)) t := match n with | O => match t as t0 return ((fun _ : type => @sigT Type (fun x : Type => x)) t0) with | Tvoid => (fun t0 : type => if type_is_by_value t0 then @existT Type (fun x : Type => x) val Vundef else @existT Type (fun x : Type => x) unit tt) Tvoid | Tint i s a => (fun t0 : type => if type_is_by_value t0 then @existT Type (fun x : Type => x) val Vundef else @existT Type (fun x : Type => x) unit tt) (Tint i s a) | Tlong s a => (fun t0 : type => if type_is_by_value t0 then @existT Type (fun x : Type => x) val Vundef else @existT Type (fun x : Type => x) unit tt) (Tlong s a) | Tfloat f a => (fun t0 : type => if type_is_by_value t0 then @existT Type (fun x : Type => x) val Vundef else @existT Type (fun x : Type => x) unit tt) (Tfloat f a) | Tpointer t0 a => (fun t1 : type => if type_is_by_value t1 then @existT Type (fun x : Type => x) val Vundef else @existT Type (fun x : Type => x) unit tt) (Tpointer t0 a) | Tarray t0 z a => (fun t1 : type => if type_is_by_value t1 then @existT Type (fun x : Type => x) val Vundef else @existT Type (fun x : Type => x) unit tt) (Tarray t0 z a) | Tfunction t0 t1 c => (fun t2 : type => if type_is_by_value t2 then @existT Type (fun x : Type => x) val Vundef else @existT Type (fun x : Type => x) unit tt) (Tfunction t0 t1 c) | Tstruct id a => match @PTree.get composite id (@cenv_cs CompSpecs) with | Some c => (fun t0 : type => if type_is_by_value t0 then @existT Type (fun x : Type => x) val Vundef else @existT Type (fun x : Type => x) unit tt) (Tstruct id a) | None => (fun (id0 : positive) (_ : attr) (TVs : @type_induction.FT_aux CompSpecs (fun _ : type => @sigT Type (fun x : Type => x)) id0) => @existT Type (fun x : Type => x) (@compact_prod_sigT_type Type (fun x : Type => x) (@type_induction.decay (prod ident type) (@sigT Type (fun x : Type => x)) (co_members (@get_co CompSpecs id0)) TVs)) (@compact_prod_sigT_value Type (fun x : Type => x) (@type_induction.decay (prod ident type) (@sigT Type (fun x : Type => x)) (co_members (@get_co CompSpecs id0)) TVs))) id a (@type_induction.ListTypeGen (prod ident type) (fun it0 : prod ident type => (fun _ : type => @sigT Type (fun x : Type => x)) (field_type (@fst ident type it0) (co_members (@get_co CompSpecs id)))) (fun it0 : prod ident type => (fun t0 : type => if type_is_by_value t0 then @existT Type (fun x : Type => x) val Vundef else @existT Type (fun x : Type => x) unit tt) (field_type (@fst ident type it0) (co_members (@get_co CompSpecs id)))) (co_members (@get_co CompSpecs id))) end | Tunion id a => match @PTree.get composite id (@cenv_cs CompSpecs) with | Some c => (fun t0 : type => if type_is_by_value t0 then @existT Type (fun x : Type => x) val Vundef else @existT Type (fun x : Type => x) unit tt) (Tunion id a) | None => (fun (id0 : positive) (_ : attr) (TVs : @type_induction.FT_aux CompSpecs (fun _ : type => @sigT Type (fun x : Type => x)) id0) => @existT Type (fun x : Type => x) (@compact_sum_sigT_type Type (fun x : Type => x) (@type_induction.decay (prod ident type) (@sigT Type (fun x : Type => x)) (co_members (@get_co CompSpecs id0)) TVs)) (@compact_sum_sigT_value Type (fun x : Type => x) (@type_induction.decay (prod ident type) (@sigT Type (fun x : Type => x)) (co_members (@get_co CompSpecs id0)) TVs))) id a (@type_induction.ListTypeGen (prod ident type) (fun it0 : prod ident type => (fun _ : type => @sigT Type (fun x : Type => x)) (field_type (@fst ident type it0) (co_members (@get_co CompSpecs id)))) (fun it0 : prod ident type => (fun t0 : type => if type_is_by_value t0 then @existT Type (fun x : Type => x) val Vundef else @existT Type (fun x : Type => x) unit tt) (field_type (@fst ident type it0) (co_members (@get_co CompSpecs id)))) (co_members (@get_co CompSpecs id))) end end | S n' => match t as t0 return ((fun _ : type => @sigT Type (fun x : Type => x)) t0) with | Tvoid => (fun t0 : type => if type_is_by_value t0 then @existT Type (fun x : Type => x) val Vundef else @existT Type (fun x : Type => x) unit tt) Tvoid | Tint i s a => (fun t0 : type => if type_is_by_value t0 then @existT Type (fun x : Type => x) val Vundef else @existT Type (fun x : Type => x) unit tt) (Tint i s a) | Tlong s a => (fun t0 : type => if type_is_by_value t0 then @existT Type (fun x : Type => x) val Vundef else @existT Type (fun x : Type => x) unit tt) (Tlong s a) | Tfloat f a => (fun t0 : type => if type_is_by_value t0 then @existT Type (fun x : Type => x) val Vundef else @existT Type (fun x : Type => x) unit tt) (Tfloat f a) | Tpointer t0 a => (fun t1 : type => if type_is_by_value t1 then @existT Type (fun x : Type => x) val Vundef else @existT Type (fun x : Type => x) unit tt) (Tpointer t0 a) | Tarray t0 n0 a => (fun (t1 : type) (n1 : Z) (_ : attr) (TV : (fun _ : type => @sigT Type (fun x : Type => x)) t1) => @existT Type (fun x : Type => x) (list (@projT1 Type (fun x : Type => x) TV)) (@list_repeat (@projT1 Type (fun x : Type => x) TV) (Z.to_nat n1) (@projT2 Type (fun x : Type => x) TV))) t0 n0 a (type_func_rec n' t0) | Tfunction t0 t1 c => (fun t2 : type => if type_is_by_value t2 then @existT Type (fun x : Type => x) val Vundef else @existT Type (fun x : Type => x) unit tt) (Tfunction t0 t1 c) | Tstruct id a => (fun (id0 : positive) (_ : attr) (TVs : @type_induction.FT_aux CompSpecs (fun _ : type => @sigT Type (fun x : Type => x)) id0) => @existT Type (fun x : Type => x) (@compact_prod_sigT_type Type (fun x : Type => x) (@type_induction.decay (prod ident type) (@sigT Type (fun x : Type => x)) (co_members (@get_co CompSpecs id0)) TVs)) (@compact_prod_sigT_value Type (fun x : Type => x) (@type_induction.decay (prod ident type) (@sigT Type (fun x : Type => x)) (co_members (@get_co CompSpecs id0)) TVs))) id a (@type_induction.ListTypeGen (prod ident type) (fun it0 : prod ident type => (fun _ : type => @sigT Type (fun x : Type => x)) (field_type (@fst ident type it0) (co_members (@get_co CompSpecs id)))) (fun it0 : prod ident type => type_func_rec n' (field_type (@fst ident type it0) (co_members (@get_co CompSpecs id)))) (co_members (@get_co CompSpecs id))) | Tunion id a => (fun (id0 : positive) (_ : attr) (TVs : @type_induction.FT_aux CompSpecs (fun _ : type => @sigT Type (fun x : Type => x)) id0) => @existT Type (fun x : Type => x) (@compact_sum_sigT_type Type (fun x : Type => x) (@type_induction.decay (prod ident type) (@sigT Type (fun x : Type => x)) (co_members (@get_co CompSpecs id0)) TVs)) (@compact_sum_sigT_value Type (fun x : Type => x) (@type_induction.decay (prod ident type) (@sigT Type (fun x : Type => x)) (co_members (@get_co CompSpecs id0)) TVs))) id a (@type_induction.ListTypeGen (prod ident type) (fun it0 : prod ident type => (fun _ : type => @sigT Type (fun x : Type => x)) (field_type (@fst ident type it0) (co_members (@get_co CompSpecs id)))) (fun it0 : prod ident type => type_func_rec n' (field_type (@fst ident type it0) (co_members (@get_co CompSpecs id)))) (co_members (@get_co CompSpecs id))) end end) (co_rank (Build_composite Struct (@cons (prod ident type) (@pair ident type _data tint) (@cons (prod ident type) (@pair ident type _next (tptr (Tstruct _elem noattr))) (@nil (prod ident type)))) noattr (Zpos (xO (xO (xO xH)))) (Zpos (xO (xO xH))) O (Zgeb0_ge0 (Zpos (xO (xO (xO xH)))) (@eq_refl bool (Z.geb (Zpos (xO (xO (xO xH)))) Z0))) (prove_alignof_two_p (Zpos (xO (xO xH))) (@eq_refl Z (Zpos (xO (xO xH))))) (prove_Zdivide (Zpos (xO (xO xH))) (Zpos (xO (xO (xO xH)))) (@eq_refl Z (Zpos (xO (xO (xO xH)))))))) (field_type (@fst ident type it) (co_members (@get_co CompSpecs _elem)))) (@pair ident type _data tint)) (@sigT Type (fun x : Type => x)) (@f_equal (list Type) Type (fun e : list Type => match e with | nil => (fun it : prod ident type => (fun _ : type => @sigT Type (fun x : Type => x)) (field_type (@fst ident type it) (co_members (@get_co CompSpecs _elem)))) (@pair ident type _data tint) | cons T l => T end) (@cons Type ((fun it : prod ident type => (fun _ : type => @sigT Type (fun x : Type => x)) (field_type (@fst ident type it) (co_members (@get_co CompSpecs _elem)))) (@pair ident type _data tint)) (@map (prod ident type) Type (fun it : prod ident type => (fun _ : type => @sigT Type (fun x : Type => x)) (field_type (@fst ident type it) (co_members (@get_co CompSpecs _elem)))) (@cons (prod ident type) (@pair ident type _next (tptr (Tstruct _elem noattr))) (@nil (prod ident type))))) (@map (prod ident type) Type (fun _ : prod ident type => @sigT Type (fun x : Type => x)) (@cons (prod ident type) (@pair ident type _data tint) (@cons (prod ident type) (@pair ident type _next (tptr (Tstruct _elem noattr))) (@nil (prod ident type))))) (@eq_refl (list Type) (@map (prod ident type) Type (fun _ : prod ident type => @sigT Type (fun x : Type => x)) (@cons (prod ident type) (@pair ident type _data tint) (@cons (prod ident type) (@pair ident type _next (tptr (Tstruct _elem noattr))) (@nil (prod ident type))))))) in (fun x : Type => x) t) val i v) p) (@sepcon mpred Nveric Sveric (@list_cell CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS sh i p) (@field_at CompSpecs sh t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) v p)) *)
   do 2 unfold_data_at (data_at _ _ _ _). cancel.
+ rewrite @lseg_cons_eq by auto.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _h hd) (@cons localdef (temp _Q q) (@nil localdef))) (SEPx (@cons mpred (@data_at CompSpecs Ews t_struct_fifo (@pair val val hd tl) q) (@cons mpred (@malloc_token CompSpecs Ews t_struct_fifo q) (@cons mpred (@andp mpred Nveric (@prop mpred Nveric (not (ptr_eq hd tl))) (@exp mpred Nveric val (fun y : val => @sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@andp mpred Nveric (@prop mpred Nveric (is_pointer_or_null y)) (@malloc_token CompSpecs Ews t_struct_elem hd)) (@list_cell CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS Ews v hd)) (@field_at CompSpecs Ews (@list_struct CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS) (@cons gfield (StructField _next) (@nil gfield)) (@valinject CompSpecs (@nested_field_type CompSpecs (@list_struct CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS) (@cons gfield (StructField _next) (@nil gfield))) y) hd)) (@lseg CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS Ews prefix y tl)))) (@cons mpred (@malloc_token CompSpecs Ews t_struct_elem tl) (@cons mpred (@data_at CompSpecs Ews t_struct_elem (@pair val val last nullval) tl) (@nil mpred))))))))) (Ssequence (Sset _n (Efield (Ederef (Etempvar _h (tptr (Tstruct _elem noattr))) (Tstruct _elem noattr)) _next (tptr (Tstruct _elem noattr)))) MORE_COMMANDS) POSTCONDITION *)
    Intros x.
    simpl @valinject. (* can we make this automatic? *)
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _h hd) (@cons localdef (temp _Q q) (@nil localdef))) (SEPx (@cons mpred (@data_at CompSpecs Ews t_struct_fifo (@pair val val hd tl) q) (@cons mpred (@malloc_token CompSpecs Ews t_struct_fifo q) (@cons mpred (@malloc_token CompSpecs Ews t_struct_elem hd) (@cons mpred (@list_cell CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS Ews v hd) (@cons mpred (@field_at CompSpecs Ews (@list_struct CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS) (@cons gfield (StructField _next) (@nil gfield)) x hd) (@cons mpred (@lseg CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS Ews prefix x tl) (@cons mpred (@malloc_token CompSpecs Ews t_struct_elem tl) (@cons mpred (@data_at CompSpecs Ews t_struct_elem (@pair val val last nullval) tl) (@nil mpred)))))))))))) (Ssequence (Sset _n (Efield (Ederef (Etempvar _h (tptr (Tstruct _elem noattr))) (Tstruct _elem noattr)) _next (tptr (Tstruct _elem noattr)))) MORE_COMMANDS) POSTCONDITION *)
    subst_any.
    forward. (*  n=h->next; *)
    forward. (* Q->head=n; *)
    forward. (* return p; *)
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Ews t_struct_fifo (@pair val val x tl) q) (@malloc_token CompSpecs Ews t_struct_fifo q)) (@malloc_token CompSpecs Ews t_struct_elem hd)) (@list_cell CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS Ews v hd)) (@field_at CompSpecs Ews (@list_struct CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS) (@cons gfield (StructField _next) (@nil gfield)) x hd)) (@lseg CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS Ews prefix x tl)) (@malloc_token CompSpecs Ews t_struct_elem tl)) (@data_at CompSpecs Ews t_struct_elem (@pair val val last nullval) tl)) (@andp mpred Nveric (@prop mpred Nveric (@eq val hd hd)) (@sepcon mpred Nveric Sveric (fifo (@app val prefix (@cons val last (@nil val))) q) (@sepcon mpred Nveric Sveric (@malloc_token CompSpecs Ews t_struct_elem hd) (@data_at CompSpecs Ews t_struct_elem (@pair val val v Vundef) hd)))) *)
    Exists hd. unfold fifo, fifo_body. Exists (x, tl).
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Ews t_struct_fifo (@pair val val x tl) q) (@malloc_token CompSpecs Ews t_struct_fifo q)) (@malloc_token CompSpecs Ews t_struct_elem hd)) (@list_cell CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS Ews v hd)) (@field_at CompSpecs Ews (@list_struct CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS) (@cons gfield (StructField _next) (@nil gfield)) x hd)) (@lseg CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS Ews prefix x tl)) (@malloc_token CompSpecs Ews t_struct_elem tl)) (@data_at CompSpecs Ews t_struct_elem (@pair val val last nullval) tl)) (@andp mpred Nveric (@prop mpred Nveric (@eq val hd hd)) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@andp mpred Nveric (@andp mpred Nveric (@prop mpred Nveric (is_pointer_or_null x)) (@prop mpred Nveric (is_pointer_or_null tl))) (@data_at CompSpecs Ews t_struct_fifo (@pair val val x tl) q)) (@malloc_token CompSpecs Ews t_struct_fifo q)) (if @isnil val (@app val prefix (@cons val last (@nil val))) then @andp mpred Nveric (@prop mpred Nveric (@eq val x nullval)) (@emp mpred Nveric Sveric) else @exp mpred Nveric (list val) (fun prefix0 : list val => @exp mpred Nveric val (fun last0 : val => @andp mpred Nveric (@prop mpred Nveric (@eq (list val) (@app val prefix (@cons val last (@nil val))) (@app val prefix0 (@cons val last0 (@nil val))))) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@lseg CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS Ews prefix0 x tl) (@malloc_token CompSpecs Ews t_struct_elem tl)) (@data_at CompSpecs Ews t_struct_elem (@pair val val last0 nullval) tl)))))) (@sepcon mpred Nveric Sveric (@malloc_token CompSpecs Ews t_struct_elem hd) (@data_at CompSpecs Ews t_struct_elem (@pair val val v Vundef) hd)))) *)
    rewrite if_false by (destruct prefix; simpl; congruence).
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Ews t_struct_fifo (@pair val val x tl) q) (@malloc_token CompSpecs Ews t_struct_fifo q)) (@malloc_token CompSpecs Ews t_struct_elem hd)) (@list_cell CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS Ews v hd)) (@field_at CompSpecs Ews (@list_struct CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS) (@cons gfield (StructField _next) (@nil gfield)) x hd)) (@lseg CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS Ews prefix x tl)) (@malloc_token CompSpecs Ews t_struct_elem tl)) (@data_at CompSpecs Ews t_struct_elem (@pair val val last nullval) tl)) (@andp mpred Nveric (@prop mpred Nveric (@eq val hd hd)) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@andp mpred Nveric (@andp mpred Nveric (@prop mpred Nveric (is_pointer_or_null x)) (@prop mpred Nveric (is_pointer_or_null tl))) (@data_at CompSpecs Ews t_struct_fifo (@pair val val x tl) q)) (@malloc_token CompSpecs Ews t_struct_fifo q)) (@exp mpred Nveric (list val) (fun prefix0 : list val => @exp mpred Nveric val (fun last0 : val => @andp mpred Nveric (@prop mpred Nveric (@eq (list val) (@app val prefix (@cons val last (@nil val))) (@app val prefix0 (@cons val last0 (@nil val))))) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@lseg CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS Ews prefix0 x tl) (@malloc_token CompSpecs Ews t_struct_elem tl)) (@data_at CompSpecs Ews t_struct_elem (@pair val val last0 nullval) tl)))))) (@sepcon mpred Nveric Sveric (@malloc_token CompSpecs Ews t_struct_elem hd) (@data_at CompSpecs Ews t_struct_elem (@pair val val v Vundef) hd)))) *)
    Exists prefix last.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (mem_mgr gv) (@malloc_token CompSpecs Ews t_struct_elem p)) (@data_at CompSpecs Ews t_struct_elem (@pair val val (Vint i) Vundef) p)) (@andp mpred Nveric (@prop mpred Nveric (@eq val p p)) (@sepcon mpred Nveric Sveric (mem_mgr gv) (@sepcon mpred Nveric Sveric (@malloc_token CompSpecs Ews t_struct_elem p) (@data_at CompSpecs Ews t_struct_elem (@pair val val (Vint i) Vundef) p)))) *)
    entailer!.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@list_cell CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS Ews v hd) (@field_at CompSpecs Ews (@list_struct CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS) (@cons gfield (StructField _next) (@nil gfield)) x hd)) (@sepcon mpred Nveric Sveric (@list_cell CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS Ews v hd) (@field_at CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) Vundef hd)) *)
    rewrite field_at_list_cell. simpl sizeof. cancel.
Qed.

Lemma body_make_elem: semax_body Vprog Gprog f_make_elem make_elem_spec.
Proof.
(* Goal: semax_body Vprog Gprog CompSpecs f_make_elem make_elem_spec *)
start_function.
forward_call (*  p = surely_malloc(sizeof ( *p));  *)
    (t_struct_elem, gv).
(* Goal: and (and (Z.le Z0 (@sizeof (@cenv_cs CompSpecs) t_struct_elem)) (Z.le (@sizeof (@cenv_cs CompSpecs) t_struct_elem) Int.max_unsigned)) (and (@eq bool (@complete_legal_cosu_type (@cenv_cs CompSpecs) t_struct_elem) true) (@eq bool (@natural_aligned CompSpecs natural_alignment t_struct_elem) true)) *)
(* Goal: semax CompSpecs Espec Delta (@exp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) val (fun vret : val => PROPx (@nil Prop) (LOCALx (@cons localdef (temp _p vret) (@cons localdef (temp _data (Vint i)) (@cons localdef (gvars gv) (@nil localdef)))) (SEPx (@cons mpred (mem_mgr gv) (@cons mpred (@sepcon mpred Nveric Sveric (@malloc_token CompSpecs Ews t_struct_elem vret) (@data_at_ CompSpecs Ews t_struct_elem vret)) (@nil mpred))))))) (Ssequence (Sassign (Efield (Ederef (Etempvar _p (tptr (Tstruct _elem noattr))) (Tstruct _elem noattr)) _data tint) (Etempvar _data tint)) MORE_COMMANDS) POSTCONDITION *)
 split3; simpl; auto; computable.
(* Goal: semax CompSpecs Espec Delta (@exp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) val (fun vret : val => PROPx (@nil Prop) (LOCALx (@cons localdef (temp _p vret) (@cons localdef (temp _data (Vint i)) (@cons localdef (gvars gv) (@nil localdef)))) (SEPx (@cons mpred (mem_mgr gv) (@cons mpred (@sepcon mpred Nveric Sveric (@malloc_token CompSpecs Ews t_struct_elem vret) (@data_at_ CompSpecs Ews t_struct_elem vret)) (@nil mpred))))))) (Ssequence (Sassign (Efield (Ederef (Etempvar _p (tptr (Tstruct _elem noattr))) (Tstruct _elem noattr)) _data tint) (Etempvar _data tint)) MORE_COMMANDS) POSTCONDITION *)
 Intros p.
forward.  (*  p->data=i; *)
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _p p) (@cons localdef (temp _data (Vint i)) (@cons localdef (gvars gv) (@nil localdef)))) (SEPx (@cons mpred (mem_mgr gv) (@cons mpred (@malloc_token CompSpecs Ews t_struct_elem p) (@cons mpred (@data_at CompSpecs Ews t_struct_elem (@pair val val (Vint i) (let (_, y) := @default_val CompSpecs t_struct_elem in y)) p) (@nil mpred))))))) (Sreturn (@Some expr (Etempvar _p (tptr (Tstruct _elem noattr))))) POSTCONDITION *)
simpl.
forward. (* return p; *)
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (mem_mgr gv) (@malloc_token CompSpecs Ews t_struct_elem p)) (@data_at CompSpecs Ews t_struct_elem (@pair val val (Vint i) Vundef) p)) (@exp mpred Nveric val (fun a : val => @andp mpred Nveric (@prop mpred Nveric (@eq val p a)) (@sepcon mpred Nveric Sveric (mem_mgr gv) (@sepcon mpred Nveric Sveric (@malloc_token CompSpecs Ews t_struct_elem a) (@data_at CompSpecs Ews t_struct_elem (@pair val val (Vint i) Vundef) a))))) *)
Exists p.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (mem_mgr gv) (@malloc_token CompSpecs Ews t_struct_elem p)) (@data_at CompSpecs Ews t_struct_elem (@pair val val (Vint i) Vundef) p)) (@andp mpred Nveric (@prop mpred Nveric (@eq val p p)) (@sepcon mpred Nveric Sveric (mem_mgr gv) (@sepcon mpred Nveric Sveric (@malloc_token CompSpecs Ews t_struct_elem p) (@data_at CompSpecs Ews t_struct_elem (@pair val val (Vint i) Vundef) p)))) *)
entailer!.
Qed.

Lemma body_main:  semax_body Vprog Gprog f_main main_spec.
Proof.
(* Goal: semax_body Vprog Gprog CompSpecs f_make_elem make_elem_spec *)
start_function.
sep_apply (create_mem_mgr gv).
forward_call (* Q = fifo_new(); *)  gv.
(* Goal: semax CompSpecs Espec Delta (@exp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) val (fun vret : val => PROPx (@nil Prop) (LOCALx (@cons localdef (temp _Q vret) (@cons localdef (gvars gv) (@nil localdef))) (SEPx (@cons mpred (mem_mgr gv) (@cons mpred (@sepcon mpred Nveric Sveric (@malloc_token CompSpecs Ews t_struct_fifo vret) (@data_at_ CompSpecs Ews t_struct_fifo vret)) (@nil mpred))))))) (Ssequence (Sassign (Efield (Ederef (Etempvar _Q (tptr (Tstruct _fifo noattr))) (Tstruct _fifo noattr)) _head (tptr (Tstruct _elem noattr))) (Ecast (Econst_int (Int.repr Z0) tint) (tptr tvoid))) MORE_COMMANDS) POSTCONDITION *)
Intros q.

forward_call  (*  p = make_elem(1); *)
     (Int.repr 1, gv).
Intros p'.
forward_call (* fifo_put(Q,p);*)
    ((q, @nil val),p', Vint (Int.repr 1)).

forward_call  (*  p = make_elem(2); *)
     (Int.repr 2, gv).
Intros p2.
simpl app.
 forward_call  (* fifo_put(Q,p); *)
    (((q,[Vint (Int.repr 1)]),p2), Vint (Int.repr 2)).
simpl app.
forward_call  (*   p' = fifo_get(Q); p = p'; *)
    ((q,[Vint (Int.repr 2)]), Vint (Int.repr 1)).
Intros p3.
forward. (*   i = p->data;  *)
forward_call (*  free(p); *)
   (t_struct_elem, p3, gv).
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@list_cell CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS Ews v hd) (@field_at CompSpecs Ews (@list_struct CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS) (@cons gfield (StructField _next) (@nil gfield)) x hd)) (@sepcon mpred Nveric Sveric (@list_cell CompSpecs _elem _next (fun _ : share => @malloc_token CompSpecs Ews t_struct_elem) QS Ews v hd) (@field_at CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) Vundef hd)) *)
assert_PROP (isptr p3); [entailer! | rewrite if_false by (intro; subst; contradiction) ]; cancel.
forward. (* return i; *)
Qed.

Existing Instance NullExtension.Espec.

Lemma prog_correct:
  semax_prog prog Vprog Gprog.
Proof.
(* Goal: semax_prog NullExtension.Espec CompSpecs prog Vprog Gprog *)
prove_semax_prog.
(* Goal: semax_func NullExtension.Espec Vprog Gprog CompSpecs (@cons (prod ident (fundef function)) (@pair ident (fundef function) _malloc (@External function EF_malloc (Tcons tuint Tnil) (tptr tvoid) cc_default)) (@cons (prod ident (fundef function)) (@pair ident (fundef function) _free (@External function EF_free (Tcons (tptr tvoid) Tnil) tvoid cc_default)) (@cons (prod ident (fundef function)) (@pair ident (fundef function) _exit (@External function (EF_external (String (Ascii.Ascii true false true false false true true false) (String (Ascii.Ascii false false false true true true true false) (String (Ascii.Ascii true false false true false true true false) (String (Ascii.Ascii false false true false true true true false) EmptyString)))) (mksignature (@cons typ AST.Tint (@nil typ)) (@None typ) cc_default)) (Tcons tint Tnil) tvoid cc_default)) (@cons (prod ident (fundef function)) (@pair ident (fundef function) _surely_malloc (@Internal function f_surely_malloc)) (@cons (prod ident (fundef function)) (@pair ident (fundef function) _fifo_new (@Internal function f_fifo_new)) (@cons (prod ident (fundef function)) (@pair ident (fundef function) _fifo_put (@Internal function f_fifo_put)) (@cons (prod ident (fundef function)) (@pair ident (fundef function) _fifo_empty (@Internal function f_fifo_empty)) (@cons (prod ident (fundef function)) (@pair ident (fundef function) _fifo_get (@Internal function f_fifo_get)) (@cons (prod ident (fundef function)) (@pair ident (fundef function) _make_elem (@Internal function f_make_elem)) (@cons (prod ident (fundef function)) (@pair ident (fundef function) _main (@Internal function f_main)) (@nil (prod ident (fundef function))))))))))))) (@cons (prod ident funspec) (@pair ident funspec _malloc (@malloc_spec' CompSpecs)) (@cons (prod ident funspec) (@pair ident funspec _free (@free_spec' CompSpecs)) (@cons (prod ident funspec) (@pair ident funspec _exit exit_spec') (@cons (prod ident funspec) (@pair ident funspec _surely_malloc (NDmk_funspec (@pair (list (prod ident type)) type (@cons (prod ident type) (@pair ident type _n tuint) (@nil (prod ident type))) (tptr tvoid)) cc_default (prod type globals) (fun x : prod type globals => let (t, gv) := x in PROPx (@cons Prop (and (Z.le Z0 (@sizeof (@cenv_cs CompSpecs) t)) (Z.le (@sizeof (@cenv_cs CompSpecs) t) Int.max_unsigned)) (@cons Prop (@eq bool (@complete_legal_cosu_type (@cenv_cs CompSpecs) t) true) (@cons Prop (@eq bool (@natural_aligned CompSpecs natural_alignment t) true) (@nil Prop)))) (LOCALx (@cons localdef (temp _n (Vint (Int.repr (@sizeof (@cenv_cs CompSpecs) t)))) (@cons localdef (gvars gv) (@nil localdef))) (SEPx (@cons mpred (mem_mgr gv) (@nil mpred))))) (fun x : prod type globals => let (t, gv) := x in @exp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) val (fun p : val => PROPx (@nil Prop) (LOCALx (@cons localdef (temp ret_temp p) (@nil localdef)) (SEPx (@cons mpred (mem_mgr gv) (@cons mpred (@sepcon mpred Nveric Sveric (@malloc_token CompSpecs Ews t p) (@data_at_ CompSpecs Ews t p)) (@nil mpred))))))))) (@cons (prod ident funspec) (@pair ident funspec _fifo_new (NDmk_funspec (@pair (list (prod ident type)) type (@nil (prod ident type)) (tptr t_struct_fifo)) cc_default globals (fun gv : globals => PROPx (@nil Prop) (LOCALx (@cons localdef (gvars gv) (@nil localdef)) (SEPx (@cons mpred (mem_mgr gv) (@nil mpred))))) (fun gv : globals => @exp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) val (fun v : val => PROPx (@nil Prop) (LOCALx (@cons localdef (temp ret_temp v) (@nil localdef)) (SEPx (@cons mpred (mem_mgr gv) (@cons mpred (fifo (@nil val) v) (@nil mpred))))))))) (@cons (prod ident funspec) (@pair ident funspec _fifo_put (NDmk_funspec (@pair (list (prod ident type)) type (@cons (prod ident type) (@pair ident type _Q (tptr t_struct_fifo)) (@cons (prod ident type) (@pair ident type _p (tptr t_struct_elem)) (@nil (prod ident type)))) tvoid) cc_default (prod (prod (prod val (list val)) val) val) (fun x : prod (prod (prod val (list val)) val) val => let (p0, last) := x in let (p1, p) := p0 in let (q, contents) := p1 in PROPx (@nil Prop) (LOCALx (@cons localdef (temp _Q q) (@cons localdef (temp _p p) (@nil localdef))) (SEPx (@cons mpred (fifo contents q) (@cons mpred (@malloc_token CompSpecs Ews t_struct_elem p) (@cons mpred (@data_at CompSpecs Ews t_struct_elem (@pair val val last Vundef) p) (@nil mpred))))))) (fun x : prod (prod (prod val (list val)) val) val => let (p0, last) := x in let (p1, _) := p0 in let (q, contents) := p1 in PROPx (@nil Prop) (LOCALx (@nil localdef) (SEPx (@cons mpred (fifo (@app val contents (@cons val last (@nil val))) q) (@nil mpred))))))) (@cons (prod ident funspec) (@pair ident funspec _fifo_empty (NDmk_funspec (@pair (list (prod ident type)) type (@cons (prod ident type) (@pair ident type _Q (tptr t_struct_fifo)) (@nil (prod ident type))) tint) cc_default (prod val (list val)) (fun x : prod val (list val) => let (q, contents) := x in PROPx (@nil Prop) (LOCALx (@cons localdef (temp _Q q) (@nil localdef)) (SEPx (@cons mpred (fifo contents q) (@nil mpred))))) (fun x : prod val (list val) => let (q, contents) := x in PROPx (@nil Prop) (LOCALx (@cons localdef (temp ret_temp (if @isnil val contents then Vtrue else Vfalse)) (@nil localdef)) (SEPx (@cons mpred (fifo contents q) (@nil mpred))))))) (@cons (prod ident funspec) (@pair ident funspec _fifo_get (NDmk_funspec (@pair (list (prod ident type)) type (@cons (prod ident type) (@pair ident type _Q (tptr t_struct_fifo)) (@nil (prod ident type))) (tptr t_struct_elem)) cc_default (prod (prod val (list val)) val) (fun x : prod (prod val (list val)) val => let (p, first) := x in let (q, contents) := p in PROPx (@nil Prop) (LOCALx (@cons localdef (temp _Q q) (@nil localdef)) (SEPx (@cons mpred (fifo (@cons val first contents) q) (@nil mpred))))) (fun x : prod (prod val (list val)) val => let (p, first) := x in let (q, contents) := p in @exp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) val (fun p0 : val => PROPx (@nil Prop) (LOCALx (@cons localdef (temp ret_temp p0) (@nil localdef)) (SEPx (@cons mpred (fifo contents q) (@cons mpred (@malloc_token CompSpecs Ews t_struct_elem p0) (@cons mpred (@data_at CompSpecs Ews t_struct_elem (@pair val val first Vundef) p0) (@nil mpred)))))))))) (@cons (prod ident funspec) (@pair ident funspec _make_elem (NDmk_funspec (@pair (list (prod ident type)) type (@cons (prod ident type) (@pair ident type _data tint) (@nil (prod ident type))) (tptr t_struct_elem)) cc_default (prod Int.int globals) (fun x : prod Int.int globals => let (i, gv) := x in PROPx (@nil Prop) (LOCALx (@cons localdef (temp _data (Vint i)) (@cons localdef (gvars gv) (@nil localdef))) (SEPx (@cons mpred (mem_mgr gv) (@nil mpred))))) (fun x : prod Int.int globals => let (i, gv) := x in @exp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) val (fun p : val => PROPx (@nil Prop) (LOCALx (@cons localdef (temp ret_temp p) (@nil localdef)) (SEPx (@cons mpred (mem_mgr gv) (@cons mpred (@malloc_token CompSpecs Ews t_struct_elem p) (@cons mpred (@data_at CompSpecs Ews t_struct_elem (@pair val val (Vint i) Vundef) p) (@nil mpred)))))))))) (@cons (prod ident funspec) (@pair ident funspec _main (NDmk_funspec (@pair (list (prod ident type)) type (@nil (prod ident type)) tint) cc_default globals (fun gv : globals => main_pre prog (@nil Type) gv) (fun _ : globals => PROPx (@nil Prop) (LOCALx (@cons localdef (temp ret_temp (Vint (Int.repr (Zpos xH)))) (@nil localdef)) (SEPx (@cons mpred (@TT mpred Nveric) (@nil mpred))))))) (@nil (prod ident funspec)))))))))))) *)
semax_func_cons body_malloc. apply semax_func_cons_malloc_aux.
(* Goal: semax_func NullExtension.Espec Vprog Gprog CompSpecs (@cons (prod ident (fundef function)) (@pair ident (fundef function) _free (@External function EF_free (Tcons (tptr tvoid) Tnil) tvoid cc_default)) (@cons (prod ident (fundef function)) (@pair ident (fundef function) _exit (@External function (EF_external (String (Ascii.Ascii true false true false false true true false) (String (Ascii.Ascii false false false true true true true false) (String (Ascii.Ascii true false false true false true true false) (String (Ascii.Ascii false false true false true true true false) EmptyString)))) (mksignature (@cons typ AST.Tint (@nil typ)) (@None typ) cc_default)) (Tcons tint Tnil) tvoid cc_default)) (@cons (prod ident (fundef function)) (@pair ident (fundef function) _surely_malloc (@Internal function f_surely_malloc)) (@cons (prod ident (fundef function)) (@pair ident (fundef function) _fifo_new (@Internal function f_fifo_new)) (@cons (prod ident (fundef function)) (@pair ident (fundef function) _fifo_put (@Internal function f_fifo_put)) (@cons (prod ident (fundef function)) (@pair ident (fundef function) _fifo_empty (@Internal function f_fifo_empty)) (@cons (prod ident (fundef function)) (@pair ident (fundef function) _fifo_get (@Internal function f_fifo_get)) (@cons (prod ident (fundef function)) (@pair ident (fundef function) _make_elem (@Internal function f_make_elem)) (@cons (prod ident (fundef function)) (@pair ident (fundef function) _main (@Internal function f_main)) (@nil (prod ident (fundef function)))))))))))) (@cons (prod ident funspec) (@pair ident funspec _free (@free_spec' CompSpecs)) (@cons (prod ident funspec) (@pair ident funspec _exit exit_spec') (@cons (prod ident funspec) (@pair ident funspec _surely_malloc (NDmk_funspec (@pair (list (prod ident type)) type (@cons (prod ident type) (@pair ident type _n tuint) (@nil (prod ident type))) (tptr tvoid)) cc_default (prod type globals) (fun x : prod type globals => let (t, gv) := x in PROPx (@cons Prop (and (Z.le Z0 (@sizeof (@cenv_cs CompSpecs) t)) (Z.le (@sizeof (@cenv_cs CompSpecs) t) Int.max_unsigned)) (@cons Prop (@eq bool (@complete_legal_cosu_type (@cenv_cs CompSpecs) t) true) (@cons Prop (@eq bool (@natural_aligned CompSpecs natural_alignment t) true) (@nil Prop)))) (LOCALx (@cons localdef (temp _n (Vint (Int.repr (@sizeof (@cenv_cs CompSpecs) t)))) (@cons localdef (gvars gv) (@nil localdef))) (SEPx (@cons mpred (mem_mgr gv) (@nil mpred))))) (fun x : prod type globals => let (t, gv) := x in @exp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) val (fun p : val => PROPx (@nil Prop) (LOCALx (@cons localdef (temp ret_temp p) (@nil localdef)) (SEPx (@cons mpred (mem_mgr gv) (@cons mpred (@sepcon mpred Nveric Sveric (@malloc_token CompSpecs Ews t p) (@data_at_ CompSpecs Ews t p)) (@nil mpred))))))))) (@cons (prod ident funspec) (@pair ident funspec _fifo_new (NDmk_funspec (@pair (list (prod ident type)) type (@nil (prod ident type)) (tptr t_struct_fifo)) cc_default globals (fun gv : globals => PROPx (@nil Prop) (LOCALx (@cons localdef (gvars gv) (@nil localdef)) (SEPx (@cons mpred (mem_mgr gv) (@nil mpred))))) (fun gv : globals => @exp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) val (fun v : val => PROPx (@nil Prop) (LOCALx (@cons localdef (temp ret_temp v) (@nil localdef)) (SEPx (@cons mpred (mem_mgr gv) (@cons mpred (fifo (@nil val) v) (@nil mpred))))))))) (@cons (prod ident funspec) (@pair ident funspec _fifo_put (NDmk_funspec (@pair (list (prod ident type)) type (@cons (prod ident type) (@pair ident type _Q (tptr t_struct_fifo)) (@cons (prod ident type) (@pair ident type _p (tptr t_struct_elem)) (@nil (prod ident type)))) tvoid) cc_default (prod (prod (prod val (list val)) val) val) (fun x : prod (prod (prod val (list val)) val) val => let (p0, last) := x in let (p1, p) := p0 in let (q, contents) := p1 in PROPx (@nil Prop) (LOCALx (@cons localdef (temp _Q q) (@cons localdef (temp _p p) (@nil localdef))) (SEPx (@cons mpred (fifo contents q) (@cons mpred (@malloc_token CompSpecs Ews t_struct_elem p) (@cons mpred (@data_at CompSpecs Ews t_struct_elem (@pair val val last Vundef) p) (@nil mpred))))))) (fun x : prod (prod (prod val (list val)) val) val => let (p0, last) := x in let (p1, _) := p0 in let (q, contents) := p1 in PROPx (@nil Prop) (LOCALx (@nil localdef) (SEPx (@cons mpred (fifo (@app val contents (@cons val last (@nil val))) q) (@nil mpred))))))) (@cons (prod ident funspec) (@pair ident funspec _fifo_empty (NDmk_funspec (@pair (list (prod ident type)) type (@cons (prod ident type) (@pair ident type _Q (tptr t_struct_fifo)) (@nil (prod ident type))) tint) cc_default (prod val (list val)) (fun x : prod val (list val) => let (q, contents) := x in PROPx (@nil Prop) (LOCALx (@cons localdef (temp _Q q) (@nil localdef)) (SEPx (@cons mpred (fifo contents q) (@nil mpred))))) (fun x : prod val (list val) => let (q, contents) := x in PROPx (@nil Prop) (LOCALx (@cons localdef (temp ret_temp (if @isnil val contents then Vtrue else Vfalse)) (@nil localdef)) (SEPx (@cons mpred (fifo contents q) (@nil mpred))))))) (@cons (prod ident funspec) (@pair ident funspec _fifo_get (NDmk_funspec (@pair (list (prod ident type)) type (@cons (prod ident type) (@pair ident type _Q (tptr t_struct_fifo)) (@nil (prod ident type))) (tptr t_struct_elem)) cc_default (prod (prod val (list val)) val) (fun x : prod (prod val (list val)) val => let (p, first) := x in let (q, contents) := p in PROPx (@nil Prop) (LOCALx (@cons localdef (temp _Q q) (@nil localdef)) (SEPx (@cons mpred (fifo (@cons val first contents) q) (@nil mpred))))) (fun x : prod (prod val (list val)) val => let (p, first) := x in let (q, contents) := p in @exp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) val (fun p0 : val => PROPx (@nil Prop) (LOCALx (@cons localdef (temp ret_temp p0) (@nil localdef)) (SEPx (@cons mpred (fifo contents q) (@cons mpred (@malloc_token CompSpecs Ews t_struct_elem p0) (@cons mpred (@data_at CompSpecs Ews t_struct_elem (@pair val val first Vundef) p0) (@nil mpred)))))))))) (@cons (prod ident funspec) (@pair ident funspec _make_elem (NDmk_funspec (@pair (list (prod ident type)) type (@cons (prod ident type) (@pair ident type _data tint) (@nil (prod ident type))) (tptr t_struct_elem)) cc_default (prod Int.int globals) (fun x : prod Int.int globals => let (i, gv) := x in PROPx (@nil Prop) (LOCALx (@cons localdef (temp _data (Vint i)) (@cons localdef (gvars gv) (@nil localdef))) (SEPx (@cons mpred (mem_mgr gv) (@nil mpred))))) (fun x : prod Int.int globals => let (i, gv) := x in @exp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) val (fun p : val => PROPx (@nil Prop) (LOCALx (@cons localdef (temp ret_temp p) (@nil localdef)) (SEPx (@cons mpred (mem_mgr gv) (@cons mpred (@malloc_token CompSpecs Ews t_struct_elem p) (@cons mpred (@data_at CompSpecs Ews t_struct_elem (@pair val val (Vint i) Vundef) p) (@nil mpred)))))))))) (@cons (prod ident funspec) (@pair ident funspec _main (NDmk_funspec (@pair (list (prod ident type)) type (@nil (prod ident type)) tint) cc_default globals (fun gv : globals => main_pre prog (@nil Type) gv) (fun _ : globals => PROPx (@nil Prop) (LOCALx (@cons localdef (temp ret_temp (Vint (Int.repr (Zpos xH)))) (@nil localdef)) (SEPx (@cons mpred (@TT mpred Nveric) (@nil mpred))))))) (@nil (prod ident funspec))))))))))) *)
semax_func_cons body_free.
(* Goal: semax_func NullExtension.Espec Vprog Gprog CompSpecs (@cons (prod ident (fundef function)) (@pair ident (fundef function) _exit (@External function (EF_external (String (Ascii.Ascii true false true false false true true false) (String (Ascii.Ascii false false false true true true true false) (String (Ascii.Ascii true false false true false true true false) (String (Ascii.Ascii false false true false true true true false) EmptyString)))) (mksignature (@cons typ AST.Tint (@nil typ)) (@None typ) cc_default)) (Tcons tint Tnil) tvoid cc_default)) (@cons (prod ident (fundef function)) (@pair ident (fundef function) _surely_malloc (@Internal function f_surely_malloc)) (@cons (prod ident (fundef function)) (@pair ident (fundef function) _fifo_new (@Internal function f_fifo_new)) (@cons (prod ident (fundef function)) (@pair ident (fundef function) _fifo_put (@Internal function f_fifo_put)) (@cons (prod ident (fundef function)) (@pair ident (fundef function) _fifo_empty (@Internal function f_fifo_empty)) (@cons (prod ident (fundef function)) (@pair ident (fundef function) _fifo_get (@Internal function f_fifo_get)) (@cons (prod ident (fundef function)) (@pair ident (fundef function) _make_elem (@Internal function f_make_elem)) (@cons (prod ident (fundef function)) (@pair ident (fundef function) _main (@Internal function f_main)) (@nil (prod ident (fundef function))))))))))) (@cons (prod ident funspec) (@pair ident funspec _exit exit_spec') (@cons (prod ident funspec) (@pair ident funspec _surely_malloc (NDmk_funspec (@pair (list (prod ident type)) type (@cons (prod ident type) (@pair ident type _n tuint) (@nil (prod ident type))) (tptr tvoid)) cc_default (prod type globals) (fun x : prod type globals => let (t, gv) := x in PROPx (@cons Prop (and (Z.le Z0 (@sizeof (@cenv_cs CompSpecs) t)) (Z.le (@sizeof (@cenv_cs CompSpecs) t) Int.max_unsigned)) (@cons Prop (@eq bool (@complete_legal_cosu_type (@cenv_cs CompSpecs) t) true) (@cons Prop (@eq bool (@natural_aligned CompSpecs natural_alignment t) true) (@nil Prop)))) (LOCALx (@cons localdef (temp _n (Vint (Int.repr (@sizeof (@cenv_cs CompSpecs) t)))) (@cons localdef (gvars gv) (@nil localdef))) (SEPx (@cons mpred (mem_mgr gv) (@nil mpred))))) (fun x : prod type globals => let (t, gv) := x in @exp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) val (fun p : val => PROPx (@nil Prop) (LOCALx (@cons localdef (temp ret_temp p) (@nil localdef)) (SEPx (@cons mpred (mem_mgr gv) (@cons mpred (@sepcon mpred Nveric Sveric (@malloc_token CompSpecs Ews t p) (@data_at_ CompSpecs Ews t p)) (@nil mpred))))))))) (@cons (prod ident funspec) (@pair ident funspec _fifo_new (NDmk_funspec (@pair (list (prod ident type)) type (@nil (prod ident type)) (tptr t_struct_fifo)) cc_default globals (fun gv : globals => PROPx (@nil Prop) (LOCALx (@cons localdef (gvars gv) (@nil localdef)) (SEPx (@cons mpred (mem_mgr gv) (@nil mpred))))) (fun gv : globals => @exp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) val (fun v : val => PROPx (@nil Prop) (LOCALx (@cons localdef (temp ret_temp v) (@nil localdef)) (SEPx (@cons mpred (mem_mgr gv) (@cons mpred (fifo (@nil val) v) (@nil mpred))))))))) (@cons (prod ident funspec) (@pair ident funspec _fifo_put (NDmk_funspec (@pair (list (prod ident type)) type (@cons (prod ident type) (@pair ident type _Q (tptr t_struct_fifo)) (@cons (prod ident type) (@pair ident type _p (tptr t_struct_elem)) (@nil (prod ident type)))) tvoid) cc_default (prod (prod (prod val (list val)) val) val) (fun x : prod (prod (prod val (list val)) val) val => let (p0, last) := x in let (p1, p) := p0 in let (q, contents) := p1 in PROPx (@nil Prop) (LOCALx (@cons localdef (temp _Q q) (@cons localdef (temp _p p) (@nil localdef))) (SEPx (@cons mpred (fifo contents q) (@cons mpred (@malloc_token CompSpecs Ews t_struct_elem p) (@cons mpred (@data_at CompSpecs Ews t_struct_elem (@pair val val last Vundef) p) (@nil mpred))))))) (fun x : prod (prod (prod val (list val)) val) val => let (p0, last) := x in let (p1, _) := p0 in let (q, contents) := p1 in PROPx (@nil Prop) (LOCALx (@nil localdef) (SEPx (@cons mpred (fifo (@app val contents (@cons val last (@nil val))) q) (@nil mpred))))))) (@cons (prod ident funspec) (@pair ident funspec _fifo_empty (NDmk_funspec (@pair (list (prod ident type)) type (@cons (prod ident type) (@pair ident type _Q (tptr t_struct_fifo)) (@nil (prod ident type))) tint) cc_default (prod val (list val)) (fun x : prod val (list val) => let (q, contents) := x in PROPx (@nil Prop) (LOCALx (@cons localdef (temp _Q q) (@nil localdef)) (SEPx (@cons mpred (fifo contents q) (@nil mpred))))) (fun x : prod val (list val) => let (q, contents) := x in PROPx (@nil Prop) (LOCALx (@cons localdef (temp ret_temp (if @isnil val contents then Vtrue else Vfalse)) (@nil localdef)) (SEPx (@cons mpred (fifo contents q) (@nil mpred))))))) (@cons (prod ident funspec) (@pair ident funspec _fifo_get (NDmk_funspec (@pair (list (prod ident type)) type (@cons (prod ident type) (@pair ident type _Q (tptr t_struct_fifo)) (@nil (prod ident type))) (tptr t_struct_elem)) cc_default (prod (prod val (list val)) val) (fun x : prod (prod val (list val)) val => let (p, first) := x in let (q, contents) := p in PROPx (@nil Prop) (LOCALx (@cons localdef (temp _Q q) (@nil localdef)) (SEPx (@cons mpred (fifo (@cons val first contents) q) (@nil mpred))))) (fun x : prod (prod val (list val)) val => let (p, first) := x in let (q, contents) := p in @exp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) val (fun p0 : val => PROPx (@nil Prop) (LOCALx (@cons localdef (temp ret_temp p0) (@nil localdef)) (SEPx (@cons mpred (fifo contents q) (@cons mpred (@malloc_token CompSpecs Ews t_struct_elem p0) (@cons mpred (@data_at CompSpecs Ews t_struct_elem (@pair val val first Vundef) p0) (@nil mpred)))))))))) (@cons (prod ident funspec) (@pair ident funspec _make_elem (NDmk_funspec (@pair (list (prod ident type)) type (@cons (prod ident type) (@pair ident type _data tint) (@nil (prod ident type))) (tptr t_struct_elem)) cc_default (prod Int.int globals) (fun x : prod Int.int globals => let (i, gv) := x in PROPx (@nil Prop) (LOCALx (@cons localdef (temp _data (Vint i)) (@cons localdef (gvars gv) (@nil localdef))) (SEPx (@cons mpred (mem_mgr gv) (@nil mpred))))) (fun x : prod Int.int globals => let (i, gv) := x in @exp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) val (fun p : val => PROPx (@nil Prop) (LOCALx (@cons localdef (temp ret_temp p) (@nil localdef)) (SEPx (@cons mpred (mem_mgr gv) (@cons mpred (@malloc_token CompSpecs Ews t_struct_elem p) (@cons mpred (@data_at CompSpecs Ews t_struct_elem (@pair val val (Vint i) Vundef) p) (@nil mpred)))))))))) (@cons (prod ident funspec) (@pair ident funspec _main (NDmk_funspec (@pair (list (prod ident type)) type (@nil (prod ident type)) tint) cc_default globals (fun gv : globals => main_pre prog (@nil Type) gv) (fun _ : globals => PROPx (@nil Prop) (LOCALx (@cons localdef (temp ret_temp (Vint (Int.repr (Zpos xH)))) (@nil localdef)) (SEPx (@cons mpred (@TT mpred Nveric) (@nil mpred))))))) (@nil (prod ident funspec)))))))))) *)
semax_func_cons body_exit.
(* Goal: semax_func NullExtension.Espec Vprog Gprog CompSpecs (@cons (prod ident (fundef function)) (@pair ident (fundef function) _surely_malloc (@Internal function f_surely_malloc)) (@cons (prod ident (fundef function)) (@pair ident (fundef function) _fifo_new (@Internal function f_fifo_new)) (@cons (prod ident (fundef function)) (@pair ident (fundef function) _fifo_put (@Internal function f_fifo_put)) (@cons (prod ident (fundef function)) (@pair ident (fundef function) _fifo_empty (@Internal function f_fifo_empty)) (@cons (prod ident (fundef function)) (@pair ident (fundef function) _fifo_get (@Internal function f_fifo_get)) (@cons (prod ident (fundef function)) (@pair ident (fundef function) _make_elem (@Internal function f_make_elem)) (@cons (prod ident (fundef function)) (@pair ident (fundef function) _main (@Internal function f_main)) (@nil (prod ident (fundef function)))))))))) (@cons (prod ident funspec) (@pair ident funspec _surely_malloc (NDmk_funspec (@pair (list (prod ident type)) type (@cons (prod ident type) (@pair ident type _n tuint) (@nil (prod ident type))) (tptr tvoid)) cc_default (prod type globals) (fun x : prod type globals => let (t, gv) := x in PROPx (@cons Prop (and (Z.le Z0 (@sizeof (@cenv_cs CompSpecs) t)) (Z.le (@sizeof (@cenv_cs CompSpecs) t) Int.max_unsigned)) (@cons Prop (@eq bool (@complete_legal_cosu_type (@cenv_cs CompSpecs) t) true) (@cons Prop (@eq bool (@natural_aligned CompSpecs natural_alignment t) true) (@nil Prop)))) (LOCALx (@cons localdef (temp _n (Vint (Int.repr (@sizeof (@cenv_cs CompSpecs) t)))) (@cons localdef (gvars gv) (@nil localdef))) (SEPx (@cons mpred (mem_mgr gv) (@nil mpred))))) (fun x : prod type globals => let (t, gv) := x in @exp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) val (fun p : val => PROPx (@nil Prop) (LOCALx (@cons localdef (temp ret_temp p) (@nil localdef)) (SEPx (@cons mpred (mem_mgr gv) (@cons mpred (@sepcon mpred Nveric Sveric (@malloc_token CompSpecs Ews t p) (@data_at_ CompSpecs Ews t p)) (@nil mpred))))))))) (@cons (prod ident funspec) (@pair ident funspec _fifo_new (NDmk_funspec (@pair (list (prod ident type)) type (@nil (prod ident type)) (tptr t_struct_fifo)) cc_default globals (fun gv : globals => PROPx (@nil Prop) (LOCALx (@cons localdef (gvars gv) (@nil localdef)) (SEPx (@cons mpred (mem_mgr gv) (@nil mpred))))) (fun gv : globals => @exp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) val (fun v : val => PROPx (@nil Prop) (LOCALx (@cons localdef (temp ret_temp v) (@nil localdef)) (SEPx (@cons mpred (mem_mgr gv) (@cons mpred (fifo (@nil val) v) (@nil mpred))))))))) (@cons (prod ident funspec) (@pair ident funspec _fifo_put (NDmk_funspec (@pair (list (prod ident type)) type (@cons (prod ident type) (@pair ident type _Q (tptr t_struct_fifo)) (@cons (prod ident type) (@pair ident type _p (tptr t_struct_elem)) (@nil (prod ident type)))) tvoid) cc_default (prod (prod (prod val (list val)) val) val) (fun x : prod (prod (prod val (list val)) val) val => let (p0, last) := x in let (p1, p) := p0 in let (q, contents) := p1 in PROPx (@nil Prop) (LOCALx (@cons localdef (temp _Q q) (@cons localdef (temp _p p) (@nil localdef))) (SEPx (@cons mpred (fifo contents q) (@cons mpred (@malloc_token CompSpecs Ews t_struct_elem p) (@cons mpred (@data_at CompSpecs Ews t_struct_elem (@pair val val last Vundef) p) (@nil mpred))))))) (fun x : prod (prod (prod val (list val)) val) val => let (p0, last) := x in let (p1, _) := p0 in let (q, contents) := p1 in PROPx (@nil Prop) (LOCALx (@nil localdef) (SEPx (@cons mpred (fifo (@app val contents (@cons val last (@nil val))) q) (@nil mpred))))))) (@cons (prod ident funspec) (@pair ident funspec _fifo_empty (NDmk_funspec (@pair (list (prod ident type)) type (@cons (prod ident type) (@pair ident type _Q (tptr t_struct_fifo)) (@nil (prod ident type))) tint) cc_default (prod val (list val)) (fun x : prod val (list val) => let (q, contents) := x in PROPx (@nil Prop) (LOCALx (@cons localdef (temp _Q q) (@nil localdef)) (SEPx (@cons mpred (fifo contents q) (@nil mpred))))) (fun x : prod val (list val) => let (q, contents) := x in PROPx (@nil Prop) (LOCALx (@cons localdef (temp ret_temp (if @isnil val contents then Vtrue else Vfalse)) (@nil localdef)) (SEPx (@cons mpred (fifo contents q) (@nil mpred))))))) (@cons (prod ident funspec) (@pair ident funspec _fifo_get (NDmk_funspec (@pair (list (prod ident type)) type (@cons (prod ident type) (@pair ident type _Q (tptr t_struct_fifo)) (@nil (prod ident type))) (tptr t_struct_elem)) cc_default (prod (prod val (list val)) val) (fun x : prod (prod val (list val)) val => let (p, first) := x in let (q, contents) := p in PROPx (@nil Prop) (LOCALx (@cons localdef (temp _Q q) (@nil localdef)) (SEPx (@cons mpred (fifo (@cons val first contents) q) (@nil mpred))))) (fun x : prod (prod val (list val)) val => let (p, first) := x in let (q, contents) := p in @exp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) val (fun p0 : val => PROPx (@nil Prop) (LOCALx (@cons localdef (temp ret_temp p0) (@nil localdef)) (SEPx (@cons mpred (fifo contents q) (@cons mpred (@malloc_token CompSpecs Ews t_struct_elem p0) (@cons mpred (@data_at CompSpecs Ews t_struct_elem (@pair val val first Vundef) p0) (@nil mpred)))))))))) (@cons (prod ident funspec) (@pair ident funspec _make_elem (NDmk_funspec (@pair (list (prod ident type)) type (@cons (prod ident type) (@pair ident type _data tint) (@nil (prod ident type))) (tptr t_struct_elem)) cc_default (prod Int.int globals) (fun x : prod Int.int globals => let (i, gv) := x in PROPx (@nil Prop) (LOCALx (@cons localdef (temp _data (Vint i)) (@cons localdef (gvars gv) (@nil localdef))) (SEPx (@cons mpred (mem_mgr gv) (@nil mpred))))) (fun x : prod Int.int globals => let (i, gv) := x in @exp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) val (fun p : val => PROPx (@nil Prop) (LOCALx (@cons localdef (temp ret_temp p) (@nil localdef)) (SEPx (@cons mpred (mem_mgr gv) (@cons mpred (@malloc_token CompSpecs Ews t_struct_elem p) (@cons mpred (@data_at CompSpecs Ews t_struct_elem (@pair val val (Vint i) Vundef) p) (@nil mpred)))))))))) (@cons (prod ident funspec) (@pair ident funspec _main (NDmk_funspec (@pair (list (prod ident type)) type (@nil (prod ident type)) tint) cc_default globals (fun gv : globals => main_pre prog (@nil Type) gv) (fun _ : globals => PROPx (@nil Prop) (LOCALx (@cons localdef (temp ret_temp (Vint (Int.repr (Zpos xH)))) (@nil localdef)) (SEPx (@cons mpred (@TT mpred Nveric) (@nil mpred))))))) (@nil (prod ident funspec))))))))) *)
semax_func_cons body_surely_malloc.
(* Goal: semax_func NullExtension.Espec Vprog Gprog CompSpecs (@cons (prod ident (fundef function)) (@pair ident (fundef function) _fifo_new (@Internal function f_fifo_new)) (@cons (prod ident (fundef function)) (@pair ident (fundef function) _fifo_put (@Internal function f_fifo_put)) (@cons (prod ident (fundef function)) (@pair ident (fundef function) _fifo_empty (@Internal function f_fifo_empty)) (@cons (prod ident (fundef function)) (@pair ident (fundef function) _fifo_get (@Internal function f_fifo_get)) (@cons (prod ident (fundef function)) (@pair ident (fundef function) _make_elem (@Internal function f_make_elem)) (@cons (prod ident (fundef function)) (@pair ident (fundef function) _main (@Internal function f_main)) (@nil (prod ident (fundef function))))))))) (@cons (prod ident funspec) (@pair ident funspec _fifo_new (NDmk_funspec (@pair (list (prod ident type)) type (@nil (prod ident type)) (tptr t_struct_fifo)) cc_default globals (fun gv : globals => PROPx (@nil Prop) (LOCALx (@cons localdef (gvars gv) (@nil localdef)) (SEPx (@cons mpred (mem_mgr gv) (@nil mpred))))) (fun gv : globals => @exp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) val (fun v : val => PROPx (@nil Prop) (LOCALx (@cons localdef (temp ret_temp v) (@nil localdef)) (SEPx (@cons mpred (mem_mgr gv) (@cons mpred (fifo (@nil val) v) (@nil mpred))))))))) (@cons (prod ident funspec) (@pair ident funspec _fifo_put (NDmk_funspec (@pair (list (prod ident type)) type (@cons (prod ident type) (@pair ident type _Q (tptr t_struct_fifo)) (@cons (prod ident type) (@pair ident type _p (tptr t_struct_elem)) (@nil (prod ident type)))) tvoid) cc_default (prod (prod (prod val (list val)) val) val) (fun x : prod (prod (prod val (list val)) val) val => let (p0, last) := x in let (p1, p) := p0 in let (q, contents) := p1 in PROPx (@nil Prop) (LOCALx (@cons localdef (temp _Q q) (@cons localdef (temp _p p) (@nil localdef))) (SEPx (@cons mpred (fifo contents q) (@cons mpred (@malloc_token CompSpecs Ews t_struct_elem p) (@cons mpred (@data_at CompSpecs Ews t_struct_elem (@pair val val last Vundef) p) (@nil mpred))))))) (fun x : prod (prod (prod val (list val)) val) val => let (p0, last) := x in let (p1, _) := p0 in let (q, contents) := p1 in PROPx (@nil Prop) (LOCALx (@nil localdef) (SEPx (@cons mpred (fifo (@app val contents (@cons val last (@nil val))) q) (@nil mpred))))))) (@cons (prod ident funspec) (@pair ident funspec _fifo_empty (NDmk_funspec (@pair (list (prod ident type)) type (@cons (prod ident type) (@pair ident type _Q (tptr t_struct_fifo)) (@nil (prod ident type))) tint) cc_default (prod val (list val)) (fun x : prod val (list val) => let (q, contents) := x in PROPx (@nil Prop) (LOCALx (@cons localdef (temp _Q q) (@nil localdef)) (SEPx (@cons mpred (fifo contents q) (@nil mpred))))) (fun x : prod val (list val) => let (q, contents) := x in PROPx (@nil Prop) (LOCALx (@cons localdef (temp ret_temp (if @isnil val contents then Vtrue else Vfalse)) (@nil localdef)) (SEPx (@cons mpred (fifo contents q) (@nil mpred))))))) (@cons (prod ident funspec) (@pair ident funspec _fifo_get (NDmk_funspec (@pair (list (prod ident type)) type (@cons (prod ident type) (@pair ident type _Q (tptr t_struct_fifo)) (@nil (prod ident type))) (tptr t_struct_elem)) cc_default (prod (prod val (list val)) val) (fun x : prod (prod val (list val)) val => let (p, first) := x in let (q, contents) := p in PROPx (@nil Prop) (LOCALx (@cons localdef (temp _Q q) (@nil localdef)) (SEPx (@cons mpred (fifo (@cons val first contents) q) (@nil mpred))))) (fun x : prod (prod val (list val)) val => let (p, first) := x in let (q, contents) := p in @exp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) val (fun p0 : val => PROPx (@nil Prop) (LOCALx (@cons localdef (temp ret_temp p0) (@nil localdef)) (SEPx (@cons mpred (fifo contents q) (@cons mpred (@malloc_token CompSpecs Ews t_struct_elem p0) (@cons mpred (@data_at CompSpecs Ews t_struct_elem (@pair val val first Vundef) p0) (@nil mpred)))))))))) (@cons (prod ident funspec) (@pair ident funspec _make_elem (NDmk_funspec (@pair (list (prod ident type)) type (@cons (prod ident type) (@pair ident type _data tint) (@nil (prod ident type))) (tptr t_struct_elem)) cc_default (prod Int.int globals) (fun x : prod Int.int globals => let (i, gv) := x in PROPx (@nil Prop) (LOCALx (@cons localdef (temp _data (Vint i)) (@cons localdef (gvars gv) (@nil localdef))) (SEPx (@cons mpred (mem_mgr gv) (@nil mpred))))) (fun x : prod Int.int globals => let (i, gv) := x in @exp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) val (fun p : val => PROPx (@nil Prop) (LOCALx (@cons localdef (temp ret_temp p) (@nil localdef)) (SEPx (@cons mpred (mem_mgr gv) (@cons mpred (@malloc_token CompSpecs Ews t_struct_elem p) (@cons mpred (@data_at CompSpecs Ews t_struct_elem (@pair val val (Vint i) Vundef) p) (@nil mpred)))))))))) (@cons (prod ident funspec) (@pair ident funspec _main (NDmk_funspec (@pair (list (prod ident type)) type (@nil (prod ident type)) tint) cc_default globals (fun gv : globals => main_pre prog (@nil Type) gv) (fun _ : globals => PROPx (@nil Prop) (LOCALx (@cons localdef (temp ret_temp (Vint (Int.repr (Zpos xH)))) (@nil localdef)) (SEPx (@cons mpred (@TT mpred Nveric) (@nil mpred))))))) (@nil (prod ident funspec)))))))) *)
semax_func_cons body_fifo_new.
(* Goal: semax_func NullExtension.Espec Vprog Gprog CompSpecs (@cons (prod ident (fundef function)) (@pair ident (fundef function) _fifo_put (@Internal function f_fifo_put)) (@cons (prod ident (fundef function)) (@pair ident (fundef function) _fifo_empty (@Internal function f_fifo_empty)) (@cons (prod ident (fundef function)) (@pair ident (fundef function) _fifo_get (@Internal function f_fifo_get)) (@cons (prod ident (fundef function)) (@pair ident (fundef function) _make_elem (@Internal function f_make_elem)) (@cons (prod ident (fundef function)) (@pair ident (fundef function) _main (@Internal function f_main)) (@nil (prod ident (fundef function)))))))) (@cons (prod ident funspec) (@pair ident funspec _fifo_put (NDmk_funspec (@pair (list (prod ident type)) type (@cons (prod ident type) (@pair ident type _Q (tptr t_struct_fifo)) (@cons (prod ident type) (@pair ident type _p (tptr t_struct_elem)) (@nil (prod ident type)))) tvoid) cc_default (prod (prod (prod val (list val)) val) val) (fun x : prod (prod (prod val (list val)) val) val => let (p0, last) := x in let (p1, p) := p0 in let (q, contents) := p1 in PROPx (@nil Prop) (LOCALx (@cons localdef (temp _Q q) (@cons localdef (temp _p p) (@nil localdef))) (SEPx (@cons mpred (fifo contents q) (@cons mpred (@malloc_token CompSpecs Ews t_struct_elem p) (@cons mpred (@data_at CompSpecs Ews t_struct_elem (@pair val val last Vundef) p) (@nil mpred))))))) (fun x : prod (prod (prod val (list val)) val) val => let (p0, last) := x in let (p1, _) := p0 in let (q, contents) := p1 in PROPx (@nil Prop) (LOCALx (@nil localdef) (SEPx (@cons mpred (fifo (@app val contents (@cons val last (@nil val))) q) (@nil mpred))))))) (@cons (prod ident funspec) (@pair ident funspec _fifo_empty (NDmk_funspec (@pair (list (prod ident type)) type (@cons (prod ident type) (@pair ident type _Q (tptr t_struct_fifo)) (@nil (prod ident type))) tint) cc_default (prod val (list val)) (fun x : prod val (list val) => let (q, contents) := x in PROPx (@nil Prop) (LOCALx (@cons localdef (temp _Q q) (@nil localdef)) (SEPx (@cons mpred (fifo contents q) (@nil mpred))))) (fun x : prod val (list val) => let (q, contents) := x in PROPx (@nil Prop) (LOCALx (@cons localdef (temp ret_temp (if @isnil val contents then Vtrue else Vfalse)) (@nil localdef)) (SEPx (@cons mpred (fifo contents q) (@nil mpred))))))) (@cons (prod ident funspec) (@pair ident funspec _fifo_get (NDmk_funspec (@pair (list (prod ident type)) type (@cons (prod ident type) (@pair ident type _Q (tptr t_struct_fifo)) (@nil (prod ident type))) (tptr t_struct_elem)) cc_default (prod (prod val (list val)) val) (fun x : prod (prod val (list val)) val => let (p, first) := x in let (q, contents) := p in PROPx (@nil Prop) (LOCALx (@cons localdef (temp _Q q) (@nil localdef)) (SEPx (@cons mpred (fifo (@cons val first contents) q) (@nil mpred))))) (fun x : prod (prod val (list val)) val => let (p, first) := x in let (q, contents) := p in @exp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) val (fun p0 : val => PROPx (@nil Prop) (LOCALx (@cons localdef (temp ret_temp p0) (@nil localdef)) (SEPx (@cons mpred (fifo contents q) (@cons mpred (@malloc_token CompSpecs Ews t_struct_elem p0) (@cons mpred (@data_at CompSpecs Ews t_struct_elem (@pair val val first Vundef) p0) (@nil mpred)))))))))) (@cons (prod ident funspec) (@pair ident funspec _make_elem (NDmk_funspec (@pair (list (prod ident type)) type (@cons (prod ident type) (@pair ident type _data tint) (@nil (prod ident type))) (tptr t_struct_elem)) cc_default (prod Int.int globals) (fun x : prod Int.int globals => let (i, gv) := x in PROPx (@nil Prop) (LOCALx (@cons localdef (temp _data (Vint i)) (@cons localdef (gvars gv) (@nil localdef))) (SEPx (@cons mpred (mem_mgr gv) (@nil mpred))))) (fun x : prod Int.int globals => let (i, gv) := x in @exp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) val (fun p : val => PROPx (@nil Prop) (LOCALx (@cons localdef (temp ret_temp p) (@nil localdef)) (SEPx (@cons mpred (mem_mgr gv) (@cons mpred (@malloc_token CompSpecs Ews t_struct_elem p) (@cons mpred (@data_at CompSpecs Ews t_struct_elem (@pair val val (Vint i) Vundef) p) (@nil mpred)))))))))) (@cons (prod ident funspec) (@pair ident funspec _main (NDmk_funspec (@pair (list (prod ident type)) type (@nil (prod ident type)) tint) cc_default globals (fun gv : globals => main_pre prog (@nil Type) gv) (fun _ : globals => PROPx (@nil Prop) (LOCALx (@cons localdef (temp ret_temp (Vint (Int.repr (Zpos xH)))) (@nil localdef)) (SEPx (@cons mpred (@TT mpred Nveric) (@nil mpred))))))) (@nil (prod ident funspec))))))) *)
semax_func_cons body_fifo_put.
(* Goal: semax_func NullExtension.Espec Vprog Gprog CompSpecs (@cons (prod ident (fundef function)) (@pair ident (fundef function) _fifo_empty (@Internal function f_fifo_empty)) (@cons (prod ident (fundef function)) (@pair ident (fundef function) _fifo_get (@Internal function f_fifo_get)) (@cons (prod ident (fundef function)) (@pair ident (fundef function) _make_elem (@Internal function f_make_elem)) (@cons (prod ident (fundef function)) (@pair ident (fundef function) _main (@Internal function f_main)) (@nil (prod ident (fundef function))))))) (@cons (prod ident funspec) (@pair ident funspec _fifo_empty (NDmk_funspec (@pair (list (prod ident type)) type (@cons (prod ident type) (@pair ident type _Q (tptr t_struct_fifo)) (@nil (prod ident type))) tint) cc_default (prod val (list val)) (fun x : prod val (list val) => let (q, contents) := x in PROPx (@nil Prop) (LOCALx (@cons localdef (temp _Q q) (@nil localdef)) (SEPx (@cons mpred (fifo contents q) (@nil mpred))))) (fun x : prod val (list val) => let (q, contents) := x in PROPx (@nil Prop) (LOCALx (@cons localdef (temp ret_temp (if @isnil val contents then Vtrue else Vfalse)) (@nil localdef)) (SEPx (@cons mpred (fifo contents q) (@nil mpred))))))) (@cons (prod ident funspec) (@pair ident funspec _fifo_get (NDmk_funspec (@pair (list (prod ident type)) type (@cons (prod ident type) (@pair ident type _Q (tptr t_struct_fifo)) (@nil (prod ident type))) (tptr t_struct_elem)) cc_default (prod (prod val (list val)) val) (fun x : prod (prod val (list val)) val => let (p, first) := x in let (q, contents) := p in PROPx (@nil Prop) (LOCALx (@cons localdef (temp _Q q) (@nil localdef)) (SEPx (@cons mpred (fifo (@cons val first contents) q) (@nil mpred))))) (fun x : prod (prod val (list val)) val => let (p, first) := x in let (q, contents) := p in @exp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) val (fun p0 : val => PROPx (@nil Prop) (LOCALx (@cons localdef (temp ret_temp p0) (@nil localdef)) (SEPx (@cons mpred (fifo contents q) (@cons mpred (@malloc_token CompSpecs Ews t_struct_elem p0) (@cons mpred (@data_at CompSpecs Ews t_struct_elem (@pair val val first Vundef) p0) (@nil mpred)))))))))) (@cons (prod ident funspec) (@pair ident funspec _make_elem (NDmk_funspec (@pair (list (prod ident type)) type (@cons (prod ident type) (@pair ident type _data tint) (@nil (prod ident type))) (tptr t_struct_elem)) cc_default (prod Int.int globals) (fun x : prod Int.int globals => let (i, gv) := x in PROPx (@nil Prop) (LOCALx (@cons localdef (temp _data (Vint i)) (@cons localdef (gvars gv) (@nil localdef))) (SEPx (@cons mpred (mem_mgr gv) (@nil mpred))))) (fun x : prod Int.int globals => let (i, gv) := x in @exp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) val (fun p : val => PROPx (@nil Prop) (LOCALx (@cons localdef (temp ret_temp p) (@nil localdef)) (SEPx (@cons mpred (mem_mgr gv) (@cons mpred (@malloc_token CompSpecs Ews t_struct_elem p) (@cons mpred (@data_at CompSpecs Ews t_struct_elem (@pair val val (Vint i) Vundef) p) (@nil mpred)))))))))) (@cons (prod ident funspec) (@pair ident funspec _main (NDmk_funspec (@pair (list (prod ident type)) type (@nil (prod ident type)) tint) cc_default globals (fun gv : globals => main_pre prog (@nil Type) gv) (fun _ : globals => PROPx (@nil Prop) (LOCALx (@cons localdef (temp ret_temp (Vint (Int.repr (Zpos xH)))) (@nil localdef)) (SEPx (@cons mpred (@TT mpred Nveric) (@nil mpred))))))) (@nil (prod ident funspec)))))) *)
semax_func_cons body_fifo_empty.
(* Goal: semax_func NullExtension.Espec Vprog Gprog CompSpecs (@cons (prod ident (fundef function)) (@pair ident (fundef function) _fifo_get (@Internal function f_fifo_get)) (@cons (prod ident (fundef function)) (@pair ident (fundef function) _make_elem (@Internal function f_make_elem)) (@cons (prod ident (fundef function)) (@pair ident (fundef function) _main (@Internal function f_main)) (@nil (prod ident (fundef function)))))) (@cons (prod ident funspec) (@pair ident funspec _fifo_get (NDmk_funspec (@pair (list (prod ident type)) type (@cons (prod ident type) (@pair ident type _Q (tptr t_struct_fifo)) (@nil (prod ident type))) (tptr t_struct_elem)) cc_default (prod (prod val (list val)) val) (fun x : prod (prod val (list val)) val => let (p, first) := x in let (q, contents) := p in PROPx (@nil Prop) (LOCALx (@cons localdef (temp _Q q) (@nil localdef)) (SEPx (@cons mpred (fifo (@cons val first contents) q) (@nil mpred))))) (fun x : prod (prod val (list val)) val => let (p, first) := x in let (q, contents) := p in @exp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) val (fun p0 : val => PROPx (@nil Prop) (LOCALx (@cons localdef (temp ret_temp p0) (@nil localdef)) (SEPx (@cons mpred (fifo contents q) (@cons mpred (@malloc_token CompSpecs Ews t_struct_elem p0) (@cons mpred (@data_at CompSpecs Ews t_struct_elem (@pair val val first Vundef) p0) (@nil mpred)))))))))) (@cons (prod ident funspec) (@pair ident funspec _make_elem (NDmk_funspec (@pair (list (prod ident type)) type (@cons (prod ident type) (@pair ident type _data tint) (@nil (prod ident type))) (tptr t_struct_elem)) cc_default (prod Int.int globals) (fun x : prod Int.int globals => let (i, gv) := x in PROPx (@nil Prop) (LOCALx (@cons localdef (temp _data (Vint i)) (@cons localdef (gvars gv) (@nil localdef))) (SEPx (@cons mpred (mem_mgr gv) (@nil mpred))))) (fun x : prod Int.int globals => let (i, gv) := x in @exp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) val (fun p : val => PROPx (@nil Prop) (LOCALx (@cons localdef (temp ret_temp p) (@nil localdef)) (SEPx (@cons mpred (mem_mgr gv) (@cons mpred (@malloc_token CompSpecs Ews t_struct_elem p) (@cons mpred (@data_at CompSpecs Ews t_struct_elem (@pair val val (Vint i) Vundef) p) (@nil mpred)))))))))) (@cons (prod ident funspec) (@pair ident funspec _main (NDmk_funspec (@pair (list (prod ident type)) type (@nil (prod ident type)) tint) cc_default globals (fun gv : globals => main_pre prog (@nil Type) gv) (fun _ : globals => PROPx (@nil Prop) (LOCALx (@cons localdef (temp ret_temp (Vint (Int.repr (Zpos xH)))) (@nil localdef)) (SEPx (@cons mpred (@TT mpred Nveric) (@nil mpred))))))) (@nil (prod ident funspec))))) *)
semax_func_cons body_fifo_get.
(* Goal: semax_func NullExtension.Espec Vprog Gprog CompSpecs (@cons (prod ident (fundef function)) (@pair ident (fundef function) _make_elem (@Internal function f_make_elem)) (@cons (prod ident (fundef function)) (@pair ident (fundef function) _main (@Internal function f_main)) (@nil (prod ident (fundef function))))) (@cons (prod ident funspec) (@pair ident funspec _make_elem (NDmk_funspec (@pair (list (prod ident type)) type (@cons (prod ident type) (@pair ident type _data tint) (@nil (prod ident type))) (tptr t_struct_elem)) cc_default (prod Int.int globals) (fun x : prod Int.int globals => let (i, gv) := x in PROPx (@nil Prop) (LOCALx (@cons localdef (temp _data (Vint i)) (@cons localdef (gvars gv) (@nil localdef))) (SEPx (@cons mpred (mem_mgr gv) (@nil mpred))))) (fun x : prod Int.int globals => let (i, gv) := x in @exp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) val (fun p : val => PROPx (@nil Prop) (LOCALx (@cons localdef (temp ret_temp p) (@nil localdef)) (SEPx (@cons mpred (mem_mgr gv) (@cons mpred (@malloc_token CompSpecs Ews t_struct_elem p) (@cons mpred (@data_at CompSpecs Ews t_struct_elem (@pair val val (Vint i) Vundef) p) (@nil mpred)))))))))) (@cons (prod ident funspec) (@pair ident funspec _main (NDmk_funspec (@pair (list (prod ident type)) type (@nil (prod ident type)) tint) cc_default globals (fun gv : globals => main_pre prog (@nil Type) gv) (fun _ : globals => PROPx (@nil Prop) (LOCALx (@cons localdef (temp ret_temp (Vint (Int.repr (Zpos xH)))) (@nil localdef)) (SEPx (@cons mpred (@TT mpred Nveric) (@nil mpred))))))) (@nil (prod ident funspec)))) *)
semax_func_cons body_make_elem.
(* Goal: semax_func NullExtension.Espec Vprog Gprog CompSpecs (@cons (prod ident (fundef function)) (@pair ident (fundef function) _main (@Internal function f_main)) (@nil (prod ident (fundef function)))) (@cons (prod ident funspec) (@pair ident funspec _main (NDmk_funspec (@pair (list (prod ident type)) type (@nil (prod ident type)) tint) cc_default globals (fun gv : globals => main_pre prog (@nil Type) gv) (fun _ : globals => PROPx (@nil Prop) (LOCALx (@cons localdef (temp ret_temp (Vint (Int.repr (Zpos xH)))) (@nil localdef)) (SEPx (@cons mpred (@TT mpred Nveric) (@nil mpred))))))) (@nil (prod ident funspec))) *)
semax_func_cons body_main.
Qed.

