Require Import VST.floyd.proofauto.
Require Import VST.floyd.library.
Require Import VST.progs.list_dt. Import Links.
Require Import VST.progs.queue.

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 _ _ => emp).
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.

Definition Qsh : share := fst (Share.split extern_retainer).
Definition Qsh' := Share.lub (snd (Share.split extern_retainer)) Share.Rsh.

Lemma writable_share_Qsh': writable_share Qsh'.
Proof.
(* Goal: writable_share Qsh' *)
unfold writable_share, Qsh', Ews.
(* Goal: @sepalg.join share Share.Join_ba a (Share.lub b Share.Rsh) (Share.lub extern_retainer Share.Rsh) *)
split.
*
(* Goal: @eq Share.t (Share.glb a (Share.lub b Share.Rsh)) Share.bot *)
(* Goal: @eq Share.t (Share.lub a (Share.lub b Share.Rsh)) (Share.lub extern_retainer Share.Rsh) *)
rewrite Share.distrib1. rewrite glb_Lsh_Rsh, Share.lub_bot.
(* Goal: @eq Share.t (Share.glb Share.Rsh extern_retainer) Share.bot *)
(* Goal: @eq Share.t (Share.lub a (Share.lub b Share.Rsh)) (Share.lub extern_retainer Share.Rsh) *)
unfold extern_retainer.
(* Goal: @sepalg.nonidentity share Share.Join_ba pa_share Qsh *)
intro. apply identity_share_bot in H.
(* Goal: @sepalg.join share Share.Join_ba (@fst Share.t Share.t (Share.split Share.Lsh)) (@snd Share.t Share.t (Share.split Share.Lsh)) Share.Lsh *)
(* Goal: @eq Share.t (Share.glb Share.Rsh Share.Lsh) Share.bot *)
(* Goal: @eq Share.t (Share.lub a (Share.lub b Share.Rsh)) (Share.lub extern_retainer Share.Rsh) *)
destruct (Share.split Share.Lsh) eqn:?H.
(* Goal: False *)
pose proof (split_join _ _ _ H0).
simpl in *.
(* Goal: False *)
destruct (Share.split t) eqn:?H.
(* Goal: False *)
pose proof (split_join _ _ _ H2).
simpl in *.
(* Goal: False *)
destruct (Share.ord_spec1 t2 Share.Lsh) as [? _].
(* Goal: False *)
spec H4. apply leq_join_sub. apply sepalg.join_sub_trans with t; eexists; eauto.
rewrite Share.glb_commute,  <- H4 in H.
(* 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))) (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) p)) (@field_at CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) (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 p (@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 => @andp mpred Nveric (@prop mpred Nveric (@eq (list val) (@app val contents (@cons val p (@nil val))) (@app val prefix (@cons val tl (@nil val))))) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@lseg CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh Ews prefix hd tl) (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) tl)) (@field_at CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) nullval tl)))))) *)
subst.
(* Goal: False *)
apply Share.split_nontrivial in H2; auto.
(* 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))) (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) p)) (@field_at CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) (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 p (@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 => @andp mpred Nveric (@prop mpred Nveric (@eq (list val) (@app val contents (@cons val p (@nil val))) (@app val prefix (@cons val tl (@nil val))))) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@lseg CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh Ews prefix hd tl) (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) tl)) (@field_at CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) nullval tl)))))) *)
subst.
(* Goal: False *)
apply Share.split_nontrivial in H0; auto.
(* Goal: False *)
clear - H0.
unfold Share.Lsh in *.
(* Goal: False *)
destruct (Share.split Share.top) eqn:?H.
simpl in *; subst.
(* Goal: False *)
apply Share.split_nontrivial in H; auto.
(* Goal: False *)
apply Share.nontrivial; auto.
*
(* Goal: @sepalg.join_sub Share.t Share.Join_ba extern_retainer (Share.lub extern_retainer Share.Rsh) *)
apply leq_join_sub.
(* Goal: Share.Ord Share.Rsh (Share.lub (@snd Share.t Share.t (Share.split extern_retainer)) Share.Rsh) *)
apply Share.lub_upper2.
Qed.

Lemma readable_share_Qsh': readable_share Qsh'.
Proof.
(* Goal: readable_share Qsh' *)
apply writable_readable_share. apply writable_share_Qsh'.
Qed.

Lemma Qsh_Qsh': sepalg.join Qsh Qsh' Ews.
Proof.
(* Goal: @sepalg.join share Share.Join_ba Qsh Qsh' Ews *)
unfold Qsh, Qsh', Ews.
(* Goal: False *)
destruct (Share.split extern_retainer) as [a b] eqn:?H.
(* 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 (and (@eq val nullval v) (not (ptr_eq nullval 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)) (@emp mpred Nveric Sveric)) (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@vund CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) nullval)) (@field_at CompSpecs Ews (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _next) (@nil gfield)) (@valinject CompSpecs (@nested_field_type CompSpecs (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _next) (@nil gfield))) y) nullval)) (@lseg CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh Ews prefix y tl))))) (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) tl)) (@field_at CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) nullval tl)) (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) p)) (@field_at CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) (Vint (Int.repr Z0)) p)) (@exp mpred Nveric (prod val val) (fun ht : prod val val => let (hd, tl0) := 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 tl0))) (@data_at CompSpecs Ews t_struct_fifo (@pair val val hd tl0) q)) (@malloc_token CompSpecs Ews t_struct_fifo q)) (if @isnil val (@app val (@app val (@cons val v prefix) (@cons val tl (@nil val))) (@cons val p (@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 => @andp mpred Nveric (@prop mpred Nveric (@eq (list val) (@app val (@app val (@cons val v prefix) (@cons val tl (@nil val))) (@cons val p (@nil val))) (@app val prefix0 (@cons val tl0 (@nil val))))) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@lseg CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh Ews prefix0 hd tl0) (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) tl0)) (@field_at CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) nullval tl0)))))) *)
simpl.
(* Goal: @sepalg.join share Share.Join_ba a (Share.lub b Share.Rsh) (Share.lub extern_retainer Share.Rsh) *)
pose proof (split_join _ _ _ H).
(* Goal: False *)
destruct H0.
(* Goal: @sepalg.join share Share.Join_ba a (Share.lub b Share.Rsh) (Share.lub extern_retainer Share.Rsh) *)
split.
(* Goal: @eq Share.t (Share.glb a (Share.lub b Share.Rsh)) Share.bot *)
(* Goal: @eq Share.t (Share.lub a (Share.lub b Share.Rsh)) (Share.lub extern_retainer Share.Rsh) *)
rewrite Share.distrib1. rewrite H0.
(* Goal: @eq Share.t (Share.lub Share.bot (Share.glb a Share.Rsh)) Share.bot *)
(* Goal: @eq Share.t (Share.lub a (Share.lub b Share.Rsh)) (Share.lub extern_retainer Share.Rsh) *)
rewrite Share.lub_commute, Share.lub_bot.
(* Goal: @eq Share.t (Share.glb a Share.Rsh) Share.bot *)
(* Goal: @eq Share.t (Share.lub a (Share.lub b Share.Rsh)) (Share.lub extern_retainer Share.Rsh) *)
rewrite Share.glb_commute.
(* Goal: @eq Share.t (Share.glb Share.Rsh a) Share.bot *)
(* Goal: @eq Share.t (Share.lub a (Share.lub b Share.Rsh)) (Share.lub extern_retainer Share.Rsh) *)
apply sub_glb_bot with extern_retainer.
(* Goal: @sepalg.join_sub Share.t Share.Join_ba extern_retainer (Share.lub extern_retainer Share.Rsh) *)
apply leq_join_sub.
(* Goal: Share.Ord a extern_retainer *)
(* Goal: @eq Share.t (Share.glb Share.Rsh extern_retainer) Share.bot *)
(* Goal: @eq Share.t (Share.lub a (Share.lub b Share.Rsh)) (Share.lub extern_retainer Share.Rsh) *)
rewrite <- H1.
(* Goal: Share.Ord extern_retainer (Share.lub extern_retainer Share.Rsh) *)
apply Share.lub_upper1.
(* Goal: @eq Share.t (Share.glb Share.Rsh extern_retainer) Share.bot *)
(* Goal: @eq Share.t (Share.lub a (Share.lub b Share.Rsh)) (Share.lub extern_retainer Share.Rsh) *)
unfold extern_retainer.
(* Goal: @eq Share.t (Share.glb Share.Rsh (@fst Share.t Share.t (Share.split Share.Lsh))) Share.bot *)
(* Goal: @eq Share.t (Share.lub a (Share.lub b Share.Rsh)) (Share.lub extern_retainer Share.Rsh) *)
apply sub_glb_bot with Share.Lsh.
(* Goal: @sepalg.join_sub share Share.Join_ba (@fst Share.t Share.t (Share.split Share.Lsh)) Share.Lsh *)
(* Goal: @eq Share.t (Share.glb Share.Rsh Share.Lsh) Share.bot *)
(* Goal: @eq Share.t (Share.lub a (Share.lub b Share.Rsh)) (Share.lub extern_retainer Share.Rsh) *)
exists (snd (Share.split Share.Lsh)).
(* Goal: @sepalg.join share Share.Join_ba (@fst Share.t Share.t (Share.split Share.Lsh)) (@snd Share.t Share.t (Share.split Share.Lsh)) Share.Lsh *)
(* Goal: @eq Share.t (Share.glb Share.Rsh Share.Lsh) Share.bot *)
(* Goal: @eq Share.t (Share.lub a (Share.lub b Share.Rsh)) (Share.lub extern_retainer Share.Rsh) *)
destruct (Share.split Share.Lsh) eqn:?H.
(* Goal: @sepalg.join share Share.Join_ba (@fst Share.t Share.t (@pair Share.t Share.t t t0)) (@snd Share.t Share.t (@pair Share.t Share.t t t0)) Share.Lsh *)
(* Goal: @eq Share.t (Share.glb Share.Rsh Share.Lsh) Share.bot *)
(* Goal: @eq Share.t (Share.lub a (Share.lub b Share.Rsh)) (Share.lub extern_retainer Share.Rsh) *)
apply split_join; auto.
(* Goal: @eq Share.t (Share.glb Share.Rsh Share.Lsh) Share.bot *)
(* Goal: @eq Share.t (Share.lub a (Share.lub b Share.Rsh)) (Share.lub extern_retainer Share.Rsh) *)
apply glb_Rsh_Lsh.
(* Goal: @eq Share.t (Share.lub a (Share.lub b Share.Rsh)) (Share.lub extern_retainer Share.Rsh) *)
rewrite <- Share.lub_assoc.
(* Goal: @eq Share.t (Share.lub (Share.lub a b) Share.Rsh) (Share.lub extern_retainer Share.Rsh) *)
rewrite H1.
(* Goal: False *)
auto.
Qed.

Lemma Qsh_not_readable: ~ readable_share Qsh.
Proof.
(* Goal: not (readable_share Qsh) *)
unfold Qsh.
apply writable_not_join_readable with Qsh';
 [ | apply writable_share_Qsh'].
(* Goal: @sepalg.joins share Share.Join_ba Qsh' (@fst Share.t Share.t (Share.split extern_retainer)) *)
exists Ews.
(* Goal: @sepalg.join share Share.Join_ba Qsh' (@fst Share.t Share.t (Share.split extern_retainer)) Ews *)
apply sepalg.join_comm.
(* Goal: @sepalg.join share Share.Join_ba (@fst Share.t Share.t (Share.split extern_retainer)) Qsh' Ews *)
apply Qsh_Qsh'.
Qed.

Hint Resolve Qsh_not_readable.


Lemma Qsh_nonempty: Qsh <> Share.bot.
Proof.
(* Goal: not (@eq share Qsh Share.bot) *)
pose proof Qsh_Qsh'.
(* Goal: @sepalg.nonidentity share Share.Join_ba pa_share Qsh *)
intro.
(* Goal: False *)
rewrite H0 in H.
(* Goal: False *)
apply sepalg.join_unit1_e in H; [ | apply bot_identity].
(* Goal: False *)
clear H0.
(* Goal: False *)
unfold Qsh', Ews in H.
(* Goal: False *)
apply (f_equal (Share.glb Share.Lsh)) in H.
(* Goal: False *)
rewrite !Share.distrib1 in H.
(* Goal: False *)
rewrite glb_Lsh_Rsh in H.
(* Goal: False *)
rewrite !Share.lub_bot in H.
(* Goal: False *)
destruct (Share.split extern_retainer) as [a b] eqn:?H.
simpl in *.
(* Goal: False *)
assert (Ha: a <> Share.bot). {
(* Goal: @sepalg.nonidentity share Share.Join_ba pa_share Qsh *)
 intro.
(* Goal: False *)
 pose proof (Share.split_nontrivial _ _ _ H0).
(* Goal: False *)
 spec H2; auto.
(* Goal: False *)
 contradiction juicy_mem.extern_retainer_neq_bot.
}
(* Goal: False *)
apply split_join in H0.
(* Goal: False *)
destruct H0.
unfold extern_retainer in *.
(* Goal: False *)
destruct (Share.split Share.Lsh) as [c d] eqn:?H.
(* Goal: False *)
apply split_join in H2.
(* Goal: False *)
destruct H2.
rewrite <- H3 in *.
(* Goal: False *)
clear H3.
simpl in *.
(* Goal: False *)
subst c.
(* Goal: False *)
rewrite (Share.glb_commute _ b) in H.
(* Goal: False *)
rewrite Share.distrib1 in H.
(* Goal: False *)
rewrite Share.glb_commute in H2.
(* Goal: False *)
rewrite (Share.lub_commute a b) in H.
(* Goal: False *)
rewrite Share.glb_absorb in H.
(* Goal: False *)
rewrite Share.lub_absorb in H.
(* Goal: False *)
rewrite Share.lub_assoc in H.
(* Goal: False *)
rewrite <- Share.distrib2 in H.
(* Goal: False *)
rewrite Share.glb_commute in H.
(* Goal: False *)
rewrite Share.glb_absorb in H.
(* Goal: False *)
rewrite H in H0.
(* Goal: False *)
rewrite Share.lub_commute in H0.
(* Goal: False *)
rewrite Share.glb_absorb in H0.
(* 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.
Qed.

Hint Resolve Qsh_nonempty : valid_pointer.

Lemma Qsh_nonidentity: sepalg.nonidentity Qsh.
Proof.
(* Goal: @sepalg.nonidentity share Share.Join_ba pa_share Qsh *)
  intro.
(* Goal: False *)
  apply identity_share_bot in H.
(* Goal: False *)
  apply Qsh_nonempty in H.
(* Goal: False *)
  auto.
Qed.

Hint Resolve Qsh_nonidentity : valid_pointer.

Lemma sub_Qsh_Ews: sepalg.join_sub Qsh Ews.
Proof.
(* Goal: @sepalg.join_sub share Share.Join_ba Qsh Ews *)
unfold Qsh, Ews.
(* Goal: @sepalg.join_sub share Share.Join_ba (@fst Share.t Share.t (Share.split extern_retainer)) (Share.lub extern_retainer Share.Rsh) *)
apply sepalg.join_sub_trans with extern_retainer.
(* Goal: @sepalg.join_sub Share.t Share.Join_ba (@fst Share.t Share.t (Share.split extern_retainer)) extern_retainer *)
(* Goal: @sepalg.join_sub Share.t Share.Join_ba extern_retainer (Share.lub extern_retainer Share.Rsh) *)
destruct (Share.split extern_retainer) eqn:?H.
(* Goal: False *)
apply split_join in H. exists t0; auto.
(* Goal: @sepalg.join_sub Share.t Share.Join_ba extern_retainer (Share.lub extern_retainer Share.Rsh) *)
apply leq_join_sub.
(* Goal: Share.Ord extern_retainer (Share.lub extern_retainer Share.Rsh) *)
apply Share.lub_upper1.
Qed.

Hint Resolve sub_Qsh_Ews: valid_pointer.

Lemma field_at_list_cell_weak:
  forall sh i j p,
   readable_share sh ->
  field_at sh list_struct [StructField _a] i p *
  field_at sh list_struct [StructField _b] j p *
  field_at_ sh list_struct [StructField _next] p
  = list_cell QS sh (i,j) p *
  field_at_ sh list_struct [StructField _next] p.
Proof.
(* Goal: forall (al : list val) (q : val), @derives mpred Nveric (fifo al q) (@prop mpred Nveric (isptr q)) *)
intros.
(* new version of proof, for constructive definition of list_cell *)
(* Goal: @eq mpred (@sepcon mpred Nveric Sveric (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Ews (@pair (@reptype CompSpecs (@nested_field_type CompSpecs (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _a) (@nil gfield)))) (@reptype CompSpecs (@nested_field_type CompSpecs (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _b) (@nil gfield)))) (Vint a) (Vint b)) p) (@field_at_ CompSpecs Ews (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _next) (@nil gfield)) p)) (@sepcon mpred Nveric Sveric (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Ews (@pair (@reptype CompSpecs (@nested_field_type CompSpecs (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _a) (@nil gfield)))) (@reptype CompSpecs (@nested_field_type CompSpecs (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _b) (@nil gfield)))) (Vint a) (Vint b)) p) (@sepcon mpred Nveric Sveric (@field_at_ CompSpecs Qsh' (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _next) (@nil gfield)) p) (@field_at_ CompSpecs Qsh t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) p))) *)
f_equal.
(* Goal: @eq mpred (@sepcon mpred Nveric Sveric (@field_at CompSpecs sh (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _a) (@nil gfield)) i p) (@field_at CompSpecs sh (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _b) (@nil gfield)) j p)) (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS sh (@pair (@reptype CompSpecs (@nested_field_type CompSpecs (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _a) (@nil gfield)))) (@reptype CompSpecs (@nested_field_type CompSpecs (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _b) (@nil gfield)))) i j) p) *)
unfold field_at, list_cell.
(* Goal: @eq mpred (@sepcon mpred Nveric Sveric (@andp mpred Nveric (@prop mpred Nveric (@field_compatible CompSpecs (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _a) (@nil gfield)) p)) (at_offset (@data_at_rec CompSpecs sh (@nested_field_type CompSpecs (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _a) (@nil gfield))) i) (@nested_field_offset CompSpecs (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _a) (@nil gfield))) p)) (@andp mpred Nveric (@prop mpred Nveric (@field_compatible CompSpecs (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _b) (@nil gfield)) p)) (at_offset (@data_at_rec CompSpecs sh (@nested_field_type CompSpecs (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _b) (@nil gfield))) j) (@nested_field_offset CompSpecs (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _b) (@nil gfield))) p))) (@andp mpred Nveric (@prop mpred Nveric (@field_compatible CompSpecs (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@nil gfield) p)) (@struct_pred (@all_but_link _next (@list_fields CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS)) (fun it : prod ident type => @reptype CompSpecs (field_type (@fst ident type it) (@list_fields CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS))) (fun (it : prod ident type) (v : @reptype CompSpecs (field_type (@fst ident type it) (@list_fields CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS))) => withspacer sh (Z.add (field_offset (@cenv_cs CompSpecs) (@fst ident type it) (@list_fields CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS)) (@sizeof (@cenv_cs CompSpecs) (field_type (@fst ident type it) (@list_fields CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS)))) (field_offset_next (@cenv_cs CompSpecs) (@fst ident type it) (@list_fields CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) 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) (_ : val) => @emp mpred Nveric Sveric) QS)) v) (field_offset (@cenv_cs CompSpecs) (@fst ident type it) (@list_fields CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS)))) (@pair (@reptype CompSpecs (@nested_field_type CompSpecs (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _a) (@nil gfield)))) (@reptype CompSpecs (@nested_field_type CompSpecs (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _b) (@nil gfield)))) i j) p)) *)
autorewrite with gather_prop.
(* Goal: @eq mpred (@sepcon mpred Nveric Sveric (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Ews (@pair (@reptype CompSpecs (@nested_field_type CompSpecs (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _a) (@nil gfield)))) (@reptype CompSpecs (@nested_field_type CompSpecs (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _b) (@nil gfield)))) (Vint a) (Vint b)) p) (@field_at_ CompSpecs Ews (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _next) (@nil gfield)) p)) (@sepcon mpred Nveric Sveric (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Ews (@pair (@reptype CompSpecs (@nested_field_type CompSpecs (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _a) (@nil gfield)))) (@reptype CompSpecs (@nested_field_type CompSpecs (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _b) (@nil gfield)))) (Vint a) (Vint b)) p) (@sepcon mpred Nveric Sveric (@field_at_ CompSpecs Qsh' (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _next) (@nil gfield)) p) (@field_at_ CompSpecs Qsh t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) p))) *)
f_equal.
(* Goal: @eq mpred (@prop mpred Nveric (and (@field_compatible CompSpecs (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _a) (@nil gfield)) p) (@field_compatible CompSpecs (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _b) (@nil gfield)) p))) (@prop mpred Nveric (@field_compatible CompSpecs (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@nil gfield) p)) *)
apply ND_prop_ext.
(* 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 (and (@eq val nullval v) (not (ptr_eq nullval 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)) (@emp mpred Nveric Sveric)) (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@vund CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) nullval)) (@field_at CompSpecs Ews (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _next) (@nil gfield)) (@valinject CompSpecs (@nested_field_type CompSpecs (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _next) (@nil gfield))) y) nullval)) (@lseg CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh Ews prefix y tl))))) (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) tl)) (@field_at CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) nullval tl)) (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) p)) (@field_at CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) (Vint (Int.repr Z0)) p)) (@exp mpred Nveric (prod val val) (fun ht : prod val val => let (hd, tl0) := 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 tl0))) (@data_at CompSpecs Ews t_struct_fifo (@pair val val hd tl0) q)) (@malloc_token CompSpecs Ews t_struct_fifo q)) (if @isnil val (@app val (@app val (@cons val v prefix) (@cons val tl (@nil val))) (@cons val p (@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 => @andp mpred Nveric (@prop mpred Nveric (@eq (list val) (@app val (@app val (@cons val v prefix) (@cons val tl (@nil val))) (@cons val p (@nil val))) (@app val prefix0 (@cons val tl0 (@nil val))))) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@lseg CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh Ews prefix0 hd tl0) (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) tl0)) (@field_at CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) nullval tl0)))))) *)
rewrite field_compatible_cons; 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 (and (@eq val nullval v) (not (ptr_eq nullval 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)) (@emp mpred Nveric Sveric)) (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@vund CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) nullval)) (@field_at CompSpecs Ews (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _next) (@nil gfield)) (@valinject CompSpecs (@nested_field_type CompSpecs (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _next) (@nil gfield))) y) nullval)) (@lseg CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh Ews prefix y tl))))) (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) tl)) (@field_at CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) nullval tl)) (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) p)) (@field_at CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) (Vint (Int.repr Z0)) p)) (@exp mpred Nveric (prod val val) (fun ht : prod val val => let (hd, tl0) := 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 tl0))) (@data_at CompSpecs Ews t_struct_fifo (@pair val val hd tl0) q)) (@malloc_token CompSpecs Ews t_struct_fifo q)) (if @isnil val (@app val (@app val (@cons val v prefix) (@cons val tl (@nil val))) (@cons val p (@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 => @andp mpred Nveric (@prop mpred Nveric (@eq (list val) (@app val (@app val (@cons val v prefix) (@cons val tl (@nil val))) (@cons val p (@nil val))) (@app val prefix0 (@cons val tl0 (@nil val))))) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@lseg CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh Ews prefix0 hd tl0) (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) tl0)) (@field_at CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) nullval tl0)))))) *)
rewrite field_compatible_cons; simpl.
(* Goal: iff (and (and (in_members _a (@cons (prod ident type) (@pair ident type _a tint) (@cons (prod ident type) (@pair ident type _b tint) (@cons (prod ident type) (@pair ident type _next (tptr (Tstruct _elem noattr))) (@nil (prod ident type)))))) (@field_compatible CompSpecs (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@nil gfield) p)) (and (in_members _b (@cons (prod ident type) (@pair ident type _a tint) (@cons (prod ident type) (@pair ident type _b tint) (@cons (prod ident type) (@pair ident type _next (tptr (Tstruct _elem noattr))) (@nil (prod ident type)))))) (@field_compatible CompSpecs (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@nil gfield) p))) (@field_compatible CompSpecs (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@nil gfield) p) *)
intuition.
(* Goal: False *)
+ left; auto.
(* Goal: False *)
+ right; left; auto.
Qed.

Lemma make_unmake:
 forall a b p,
 data_at Ews t_struct_elem (Vint a, (Vint b, Vundef)) p =
 field_at Qsh' t_struct_elem [StructField _a] (Vint a) p *
 field_at Qsh' t_struct_elem [StructField _b] (Vint b) p *
 list_cell QS Qsh (Vundef, Vundef) p *
 field_at_ Ews t_struct_elem [StructField _next] 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 Ews t_struct_elem (@pair val (prod val val) (Vint a) (@pair val val (Vint b) Vundef)) p) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@field_at CompSpecs Qsh' t_struct_elem (@cons gfield (StructField _a) (@nil gfield)) (Vint a) p) (@field_at CompSpecs Qsh' t_struct_elem (@cons gfield (StructField _b) (@nil gfield)) (Vint b) p)) (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) p)) (@field_at_ CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) p)) *)
unfold_data_at (data_at _ _ _ _).
(* Goal: @eq mpred J (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@field_at CompSpecs Qsh' t_struct_elem (@cons gfield (StructField _a) (@nil gfield)) (Vint a) p) (@field_at CompSpecs Qsh' t_struct_elem (@cons gfield (StructField _b) (@nil gfield)) (Vint b) p)) (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) p)) (@sepcon mpred Nveric Sveric (@field_at CompSpecs Qsh t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) Vundef p) (@field_at CompSpecs Qsh' t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) Vundef p))) *)
rewrite <- !sepcon_assoc.
(* Goal: @eq mpred (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@field_at CompSpecs Ews t_struct_elem (@cons gfield (StructField _a) (@nil gfield)) (Vint a) p) (@field_at CompSpecs Ews t_struct_elem (@cons gfield (StructField _b) (@nil gfield)) (Vint b) p)) (@field_at CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) Vundef p)) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@field_at CompSpecs Qsh' t_struct_elem (@cons gfield (StructField _a) (@nil gfield)) (Vint a) p) (@field_at CompSpecs Qsh' t_struct_elem (@cons gfield (StructField _b) (@nil gfield)) (Vint b) p)) (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) p)) (@field_at_ CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) p)) *)
match goal with |- ?A = _ => set (J := A) end.
(* Goal: @eq mpred (@field_at_ CompSpecs Ews (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _next) (@nil gfield)) p) (@sepcon mpred Nveric Sveric (@field_at_ CompSpecs Qsh' (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _next) (@nil gfield)) p) (@field_at_ CompSpecs Qsh t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) p)) *)
unfold field_at_.
(* Goal: @eq mpred (@field_at CompSpecs Ews (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _next) (@nil gfield)) (@default_val CompSpecs (@nested_field_type CompSpecs (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _next) (@nil gfield)))) p) (@sepcon mpred Nveric Sveric (@field_at CompSpecs Qsh' (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _next) (@nil gfield)) (@default_val CompSpecs (@nested_field_type CompSpecs (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _next) (@nil gfield)))) p) (@field_at CompSpecs Qsh t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) (@default_val CompSpecs (@nested_field_type CompSpecs t_struct_elem (@cons gfield (StructField _next) (@nil gfield)))) p)) *)
change (default_val (nested_field_type t_struct_elem [StructField _next])) with Vundef.
(* Goal: @eq mpred J (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@field_at CompSpecs Qsh' t_struct_elem (@cons gfield (StructField _a) (@nil gfield)) (Vint a) p) (@field_at CompSpecs Qsh' t_struct_elem (@cons gfield (StructField _b) (@nil gfield)) (Vint b) p)) (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) p)) (@field_at CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) Vundef p)) *)
rewrite <- (field_at_share_join _ _ _ _ _ _ _ Qsh_Qsh').
(* Goal: @eq mpred J (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@field_at CompSpecs Qsh' t_struct_elem (@cons gfield (StructField _a) (@nil gfield)) (Vint a) p) (@field_at CompSpecs Qsh' t_struct_elem (@cons gfield (StructField _b) (@nil gfield)) (Vint b) p)) (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) p)) (@sepcon mpred Nveric Sveric (@field_at CompSpecs Qsh t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) Vundef p) (@field_at CompSpecs Qsh' t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) Vundef p))) *)
rewrite <- !sepcon_assoc.
(* Goal: @eq mpred J (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@field_at CompSpecs Qsh' t_struct_elem (@cons gfield (StructField _a) (@nil gfield)) (Vint a) p) (@field_at CompSpecs Qsh' t_struct_elem (@cons gfield (StructField _b) (@nil gfield)) (Vint b) p)) (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) p)) (@field_at CompSpecs Qsh t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) Vundef p)) (@field_at CompSpecs Qsh' t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) Vundef p)) *)
pull_left (field_at Qsh' t_struct_elem [StructField _next] Vundef p).
(* Goal: @eq mpred J (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@field_at CompSpecs Qsh' t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) Vundef p) (@field_at CompSpecs Qsh' t_struct_elem (@cons gfield (StructField _a) (@nil gfield)) (Vint a) p)) (@field_at CompSpecs Qsh' t_struct_elem (@cons gfield (StructField _b) (@nil gfield)) (Vint b) p)) (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) p)) (@field_at CompSpecs Qsh t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) Vundef p)) *)
pull_left (field_at Qsh' t_struct_elem [StructField _b] (Vint b) p).
(* Goal: @eq mpred J (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@field_at CompSpecs Qsh' t_struct_elem (@cons gfield (StructField _b) (@nil gfield)) (Vint b) p) (@field_at CompSpecs Qsh' t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) Vundef p)) (@field_at CompSpecs Qsh' t_struct_elem (@cons gfield (StructField _a) (@nil gfield)) (Vint a) p)) (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) p)) (@field_at CompSpecs Qsh t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) Vundef p)) *)
pull_left (field_at Qsh' t_struct_elem [StructField _a] (Vint a) p).
rewrite field_at_list_cell_weak  by apply readable_share_Qsh'.
match goal with |- _ = _ * _ * _ * ?A => change A
  with (field_at_ Qsh t_struct_elem [StructField _next] p)
end.
(* Goal: @eq mpred J (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh' (@pair (@reptype CompSpecs (@nested_field_type CompSpecs (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _a) (@nil gfield)))) (@reptype CompSpecs (@nested_field_type CompSpecs (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _b) (@nil gfield)))) (Vint a) (Vint b)) p) (@field_at_ CompSpecs Qsh' (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _next) (@nil gfield)) p)) (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) p)) (@field_at_ CompSpecs Qsh t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) p)) *)
pull_left (list_cell QS Qsh (Vundef, Vundef) p).
(* Goal: @eq mpred J (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) p) (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh' (@pair (@reptype CompSpecs (@nested_field_type CompSpecs (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _a) (@nil gfield)))) (@reptype CompSpecs (@nested_field_type CompSpecs (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _b) (@nil gfield)))) (Vint a) (Vint b)) p)) (@field_at_ CompSpecs Qsh' (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _next) (@nil gfield)) p)) (@field_at_ CompSpecs Qsh t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) p)) *)
rewrite join_cell_link with (psh:=Ews) by (auto; try apply Qsh_Qsh'; apply readable_share_Qsh').
(* Goal: @eq mpred J (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Ews (@pair (@reptype CompSpecs (@nested_field_type CompSpecs (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _a) (@nil gfield)))) (@reptype CompSpecs (@nested_field_type CompSpecs (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _b) (@nil gfield)))) (Vint a) (Vint b)) p) (@field_at_ CompSpecs Qsh' (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _next) (@nil gfield)) p)) (@field_at_ CompSpecs Qsh t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) p)) *)
subst J.
match goal with |- _ * _ * ?A = _ => change A
  with (field_at_ Ews t_struct_elem [StructField _next] p)
end.
(* Goal: False *)
rewrite field_at_list_cell_weak by auto.
(* Goal: @eq mpred (@sepcon mpred Nveric Sveric (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Ews (@pair (@reptype CompSpecs (@nested_field_type CompSpecs (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _a) (@nil gfield)))) (@reptype CompSpecs (@nested_field_type CompSpecs (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _b) (@nil gfield)))) (Vint a) (Vint b)) p) (@field_at_ CompSpecs Ews (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _next) (@nil gfield)) p)) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Ews (@pair (@reptype CompSpecs (@nested_field_type CompSpecs (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _a) (@nil gfield)))) (@reptype CompSpecs (@nested_field_type CompSpecs (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _b) (@nil gfield)))) (Vint a) (Vint b)) p) (@field_at_ CompSpecs Qsh' (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _next) (@nil gfield)) p)) (@field_at_ CompSpecs Qsh t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) p)) *)
rewrite sepcon_assoc.
(* Goal: @eq mpred (@sepcon mpred Nveric Sveric (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Ews (@pair (@reptype CompSpecs (@nested_field_type CompSpecs (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _a) (@nil gfield)))) (@reptype CompSpecs (@nested_field_type CompSpecs (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _b) (@nil gfield)))) (Vint a) (Vint b)) p) (@field_at_ CompSpecs Ews (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _next) (@nil gfield)) p)) (@sepcon mpred Nveric Sveric (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Ews (@pair (@reptype CompSpecs (@nested_field_type CompSpecs (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _a) (@nil gfield)))) (@reptype CompSpecs (@nested_field_type CompSpecs (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _b) (@nil gfield)))) (Vint a) (Vint b)) p) (@sepcon mpred Nveric Sveric (@field_at_ CompSpecs Qsh' (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _next) (@nil gfield)) p) (@field_at_ CompSpecs Qsh t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) p))) *)
f_equal.
(* Goal: @eq mpred (@field_at_ CompSpecs Ews (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _next) (@nil gfield)) p) (@sepcon mpred Nveric Sveric (@field_at_ CompSpecs Qsh' (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _next) (@nil gfield)) p) (@field_at_ CompSpecs Qsh t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) p)) *)
unfold field_at_.
(* Goal: @eq mpred (@field_at CompSpecs Ews (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _next) (@nil gfield)) (@default_val CompSpecs (@nested_field_type CompSpecs (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _next) (@nil gfield)))) p) (@sepcon mpred Nveric Sveric (@field_at CompSpecs Qsh' (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _next) (@nil gfield)) (@default_val CompSpecs (@nested_field_type CompSpecs (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _next) (@nil gfield)))) p) (@field_at CompSpecs Qsh t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) (@default_val CompSpecs (@nested_field_type CompSpecs t_struct_elem (@cons gfield (StructField _next) (@nil gfield)))) p)) *)
change (default_val (nested_field_type t_struct_elem [StructField _next])) with Vundef.
(* Goal: @eq mpred (@field_at CompSpecs Ews (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _next) (@nil gfield)) (@default_val CompSpecs (@nested_field_type CompSpecs (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _next) (@nil gfield)))) p) (@sepcon mpred Nveric Sveric (@field_at CompSpecs Qsh' (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _next) (@nil gfield)) (@default_val CompSpecs (@nested_field_type CompSpecs (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _next) (@nil gfield)))) p) (@field_at CompSpecs Qsh t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) Vundef p)) *)
rewrite sepcon_comm.
(* Goal: @eq mpred (@field_at CompSpecs Ews (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _next) (@nil gfield)) (@default_val CompSpecs (@nested_field_type CompSpecs (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _next) (@nil gfield)))) p) (@sepcon mpred Nveric Sveric (@field_at CompSpecs Qsh t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) Vundef p) (@field_at CompSpecs Qsh' (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _next) (@nil gfield)) (@default_val CompSpecs (@nested_field_type CompSpecs (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _next) (@nil gfield)))) p)) *)
symmetry.
apply (field_at_share_join _ _ _ t_struct_elem [StructField _next]
   _ p Qsh_Qsh').
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 elemrep (rep: elemtype QS) (p: val) : mpred :=
  field_at Ews t_struct_elem [StructField _a] (fst rep) p *
  (field_at Ews t_struct_elem [StructField _b] (snd rep) p *
   (field_at_ Ews t_struct_elem [StructField _next]) p).

Definition fifo_body (contents: list val) (hd tl: val) :=
      (if isnil contents
      then (!!(hd=nullval) && emp)
      else (EX prefix: list val,
              !!(contents = prefix++tl::nil)
            &&  (lseg QS Qsh Ews prefix hd tl
                   * list_cell QS Qsh (Vundef,Vundef) tl
                   * field_at Ews t_struct_elem [StructField _next] 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
  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;
                 list_cell QS Qsh (Vundef, Vundef) p;
                 field_at_ Ews t_struct_elem [StructField _next] p)
  POST [ tvoid ]
          PROP() LOCAL() SEP (fifo (contents++(p :: 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, p: val
  PRE  [ _Q OF (tptr t_struct_fifo) ]
       PROP() LOCAL (temp _Q q) SEP (fifo (p :: contents) q)
  POST [ (tptr t_struct_elem) ]
       PROP ()
       LOCAL(temp ret_temp p)
       SEP (fifo contents q;
              list_cell QS Qsh (Vundef, Vundef) p;
              field_at_ Ews t_struct_elem [StructField _next] p).

Definition make_elem_spec :=
 DECLARE _make_elem
  WITH a: int, b: int, gv: globals
  PRE  [ _a OF tint, _b OF tint ]
        PROP() 
        LOCAL(temp _a (Vint a); temp _b (Vint b); gvars gv) 
        SEP(mem_mgr gv)
  POST [ (tptr t_struct_elem) ]
      @exp (environ->mpred) _ _ (fun p:val =>  (* EX notation doesn't work for some reason *)
       PROP()
       LOCAL (temp ret_temp p)
       SEP (mem_mgr gv;
              field_at Qsh' list_struct [StructField _a] (Vint a) p;
              field_at Qsh' list_struct [StructField _b] (Vint b) p;
              list_cell QS Qsh (Vundef, Vundef) p;
              field_at_ Ews t_struct_elem [StructField _next] p;
              malloc_token Ews t_struct_elem 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+10)))) 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 _a (Vint a0)) (@cons localdef (temp _b (Vint b0)) (@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)) _a tint) (Etempvar _a 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 (prod val val) (Vint a0) (@pair val val (Vint b0) Vundef)) p)) (@andp mpred Nveric (@prop mpred Nveric (@eq val p p)) (@sepcon mpred Nveric Sveric (mem_mgr gv) (@sepcon mpred Nveric Sveric (@field_at CompSpecs Qsh' (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _a) (@nil gfield)) (Vint a0) p) (@sepcon mpred Nveric Sveric (@field_at CompSpecs Qsh' (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _b) (@nil gfield)) (Vint b0) p) (@sepcon mpred Nveric Sveric (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) p) (@sepcon mpred Nveric Sveric (@field_at_ CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) p) (@malloc_token CompSpecs Ews t_struct_elem 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.
    + forward. subst p. congruence.
    + 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 (prod val val) (Vint a0) (@pair val val (Vint b0) Vundef)) p)) (@andp mpred Nveric (@prop mpred Nveric (@eq val p p)) (@sepcon mpred Nveric Sveric (mem_mgr gv) (@sepcon mpred Nveric Sveric (@field_at CompSpecs Qsh' (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _a) (@nil gfield)) (Vint a0) p) (@sepcon mpred Nveric Sveric (@field_at CompSpecs Qsh' (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _b) (@nil gfield)) (Vint b0) p) (@sepcon mpred Nveric Sveric (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) p) (@sepcon mpred Nveric Sveric (@field_at_ CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) p) (@malloc_token CompSpecs Ews t_struct_elem 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 (@data_at CompSpecs Ews t_struct_fifo (@pair val val x tl) q) (@malloc_token CompSpecs Ews t_struct_fifo q)) (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@vund CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) v)) (@field_at CompSpecs Ews (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _next) (@nil gfield)) x v)) (@lseg CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh Ews prefix x tl)) (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) tl)) (@field_at CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) nullval tl)) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (fifo (@app val prefix (@cons val tl (@nil val))) q) (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) v)) (@field_at_ CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) v)) *)
 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 (prod val val) (Vint a0) (@pair val val (Vint b0) Vundef)) p)) (@andp mpred Nveric (@prop mpred Nveric (@eq val p p)) (@sepcon mpred Nveric Sveric (mem_mgr gv) (@sepcon mpred Nveric Sveric (@field_at CompSpecs Qsh' (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _a) (@nil gfield)) (Vint a0) p) (@sepcon mpred Nveric Sveric (@field_at CompSpecs Qsh' (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _b) (@nil gfield)) (Vint b0) p) (@sepcon mpred Nveric Sveric (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) p) (@sepcon mpred Nveric Sveric (@field_at_ CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) p) (@malloc_token CompSpecs Ews t_struct_elem 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 p 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 => @andp mpred Nveric (@prop mpred Nveric (@eq (list val) (@cons val p contents) (@app val prefix (@cons val tl (@nil val))))) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@lseg CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh Ews prefix hd tl) (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) tl)) (@field_at CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) 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 (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) tl) (@cons mpred (@field_at CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) 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 (mem_mgr gv) (@malloc_token CompSpecs Ews t_struct_elem p)) (@data_at CompSpecs Ews t_struct_elem (@pair val (prod val val) (Vint a0) (@pair val val (Vint b0) Vundef)) p)) (@andp mpred Nveric (@prop mpred Nveric (@eq val p p)) (@sepcon mpred Nveric Sveric (mem_mgr gv) (@sepcon mpred Nveric Sveric (@field_at CompSpecs Qsh' (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _a) (@nil gfield)) (Vint a0) p) (@sepcon mpred Nveric Sveric (@field_at CompSpecs Qsh' (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _b) (@nil gfield)) (Vint b0) p) (@sepcon mpred Nveric Sveric (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) p) (@sepcon mpred Nveric Sveric (@field_at_ CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) p) (@malloc_token CompSpecs Ews t_struct_elem p))))))) *)
entailer!.
(* 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 (@data_at CompSpecs Ews t_struct_fifo (@pair val val x tl) q) (@malloc_token CompSpecs Ews t_struct_fifo q)) (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@vund CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) v)) (@field_at CompSpecs Ews (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _next) (@nil gfield)) x v)) (@lseg CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh Ews prefix x tl)) (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) tl)) (@field_at CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) nullval tl)) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (fifo (@app val prefix (@cons val tl (@nil val))) q) (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) v)) (@field_at_ CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) v)) *)
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 => @andp mpred Nveric (@prop mpred Nveric (@eq (list val) contents (@app val prefix (@cons val tl (@nil val))))) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@lseg CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh Ews prefix hd tl) (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) tl)) (@field_at CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) nullval tl)))) (@cons mpred (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) p) (@cons mpred (@field_at CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) (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.
+ 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 (prod val val) (Vint a0) (@pair val val (Vint b0) Vundef)) p)) (@andp mpred Nveric (@prop mpred Nveric (@eq val p p)) (@sepcon mpred Nveric Sveric (mem_mgr gv) (@sepcon mpred Nveric Sveric (@field_at CompSpecs Qsh' (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _a) (@nil gfield)) (Vint a0) p) (@sepcon mpred Nveric Sveric (@field_at CompSpecs Qsh' (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _b) (@nil gfield)) (Vint b0) p) (@sepcon mpred Nveric Sveric (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) p) (@sepcon mpred Nveric Sveric (@field_at_ CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) p) (@malloc_token CompSpecs Ews t_struct_elem 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 (@data_at CompSpecs Ews t_struct_fifo (@pair val val x tl) q) (@malloc_token CompSpecs Ews t_struct_fifo q)) (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@vund CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) v)) (@field_at CompSpecs Ews (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _next) (@nil gfield)) x v)) (@lseg CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh Ews prefix x tl)) (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) tl)) (@field_at CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) nullval tl)) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (fifo (@app val prefix (@cons val tl (@nil val))) q) (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) v)) (@field_at_ CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) v)) *)
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 => @andp mpred Nveric (@prop mpred Nveric (@eq (list val) contents (@app val prefix (@cons val tl (@nil val))))) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@lseg CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh Ews prefix hd tl) (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) tl)) (@field_at CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) 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 => @andp mpred Nveric (@prop mpred Nveric (@eq (list val) contents (@app val prefix (@cons val tl (@nil val))))) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@lseg CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh Ews prefix hd tl) (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) tl)) (@field_at CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) 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 => @andp mpred Nveric (@prop mpred Nveric (@eq (list val) contents (@app val prefix (@cons val tl (@nil val))))) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@lseg CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh Ews prefix hd tl) (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) tl)) (@field_at CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) nullval tl)))) (@cons mpred (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) p) (@cons mpred (@field_at CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) (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.
(* 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 x tl) q) (@malloc_token CompSpecs Ews t_struct_fifo q)) (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@vund CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) v)) (@field_at CompSpecs Ews (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _next) (@nil gfield)) x v)) (@lseg CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh Ews prefix x tl)) (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) tl)) (@field_at CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) nullval tl)) (@sepcon mpred Nveric Sveric (@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 => @andp mpred Nveric (@prop mpred Nveric (@eq (list val) (@app val prefix (@cons val tl (@nil val))) (@app val prefix0 (@cons val tl (@nil val))))) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@lseg CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh Ews prefix0 x tl) (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) tl)) (@field_at CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) nullval tl))))) (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) v)) (@field_at_ CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) v)) *)
Exists prefix.
(* 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) (_ : val) => @emp mpred Nveric Sveric) QS Qsh Ews prefix hd tl) (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) tl)) (@field_at CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) 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 tl (@nil val))))) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@lseg CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh Ews prefix hd tl) (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) tl)) (@field_at CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) 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) (_ : val) => @emp mpred Nveric Sveric) QS Qsh Ews prefix hd tl) (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) tl)) (@field_at CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) 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) (_ : val) => @emp mpred Nveric Sveric) QS Qsh Ews prefix hd tl) (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) tl)) (@field_at CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) 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 tl (@nil val))))) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@lseg CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh Ews prefix hd tl) (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) tl)) (@field_at CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) nullval tl))))) *)
    destruct prefix; entailer.
(* Goal: False *)
    rewrite lseg_cons_eq by auto. Intros y. subst v.
(* 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) (_ : val) => @emp mpred Nveric Sveric) QS Qsh Ews prefix hd tl)) (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) tl)) (@field_at CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) p tl)) (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) p)) (@field_at CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) (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 tl (@nil val))) (@cons val p (@nil val))) (@app val (@app val prefix (@cons val tl (@nil val))) (@cons val p (@nil val))))) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@lseg CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh Ews (@app val prefix (@cons val tl (@nil val))) hd p) (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) p)) (@field_at CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) 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 (prod val val) (Vint a0) (@pair val val (Vint b0) Vundef)) p)) (@andp mpred Nveric (@prop mpred Nveric (@eq val p p)) (@sepcon mpred Nveric Sveric (mem_mgr gv) (@sepcon mpred Nveric Sveric (@field_at CompSpecs Qsh' (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _a) (@nil gfield)) (Vint a0) p) (@sepcon mpred Nveric Sveric (@field_at CompSpecs Qsh' (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _b) (@nil gfield)) (Vint b0) p) (@sepcon mpred Nveric Sveric (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) p) (@sepcon mpred Nveric Sveric (@field_at_ CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) p) (@malloc_token CompSpecs Ews t_struct_elem 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).
  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.
  forward. (* Q->head = NULL; *)
  (* goal_4 *)
  forward. (* Q->tail = NULL; *)
  forward. (* return Q; *)
  (* goal_5 *)
(* 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 x tl) q) (@malloc_token CompSpecs Ews t_struct_fifo q)) (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@vund CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) v)) (@field_at CompSpecs Ews (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _next) (@nil gfield)) x v)) (@lseg CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh Ews prefix x tl)) (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) tl)) (@field_at CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) nullval tl)) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (fifo (@app val prefix (@cons val tl (@nil val))) q) (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) v)) (@field_at_ CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) v)) *)
  Exists q. unfold fifo, fifo_body. Exists (nullval,nullval).
(* Goal: False *)
  rewrite if_true 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 (prod val val) (Vint a0) (@pair val val (Vint b0) Vundef)) p)) (@andp mpred Nveric (@prop mpred Nveric (@eq val p p)) (@sepcon mpred Nveric Sveric (mem_mgr gv) (@sepcon mpred Nveric Sveric (@field_at CompSpecs Qsh' (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _a) (@nil gfield)) (Vint a0) p) (@sepcon mpred Nveric Sveric (@field_at CompSpecs Qsh' (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _b) (@nil gfield)) (Vint b0) p) (@sepcon mpred Nveric Sveric (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) p) (@sepcon mpred Nveric Sveric (@field_at_ CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) p) (@malloc_token CompSpecs Ews t_struct_elem 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 (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) p) (@cons mpred (@field_at_ CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) 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 p 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 => @andp mpred Nveric (@prop mpred Nveric (@eq (list val) (@cons val p contents) (@app val prefix (@cons val tl (@nil val))))) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@lseg CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh Ews prefix hd tl) (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) tl)) (@field_at CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) 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 (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) tl) (@cons mpred (@field_at CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) 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 ++ p :: nil) q))%assert.
* unfold fifo_body.
   if_tac; entailer.  (* typechecking clause *)
    (* entailer! should perhaps solve this one too *)
* (* 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))) (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) p)) (@field_at CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) (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 p (@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 => @andp mpred Nveric (@prop mpred Nveric (@eq (list val) (@app val contents (@cons val p (@nil val))) (@app val prefix (@cons val tl (@nil val))))) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@lseg CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh Ews prefix hd tl) (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) tl)) (@field_at CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) nullval tl)))))) *)
  subst.
  (* goal 9 *)
  forward. (* Q->head=p; *)
  forward. (* Q->tail=p; *)
  (* goal 10 *)
(* 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) (_ : val) => @emp mpred Nveric Sveric) QS Qsh Ews prefix hd tl)) (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) tl)) (@field_at CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) p tl)) (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) p)) (@field_at CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) (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 tl (@nil val))) (@cons val p (@nil val))) (@app val (@app val prefix (@cons val tl (@nil val))) (@cons val p (@nil val))))) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@lseg CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh Ews (@app val prefix (@cons val tl (@nil val))) hd p) (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) p)) (@field_at CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) 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 x tl) q) (@malloc_token CompSpecs Ews t_struct_fifo q)) (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@vund CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) v)) (@field_at CompSpecs Ews (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _next) (@nil gfield)) x v)) (@lseg CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh Ews prefix x tl)) (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) tl)) (@field_at CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) nullval tl)) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (fifo (@app val prefix (@cons val tl (@nil val))) q) (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) v)) (@field_at_ CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) v)) *)
  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 => @andp mpred Nveric (@prop mpred Nveric (@eq (list val) contents (@app val prefix (@cons val tl (@nil val))))) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@lseg CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh Ews prefix hd tl) (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) tl)) (@field_at CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) nullval tl)))) (@cons mpred (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) p) (@cons mpred (@field_at CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) (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).
(* 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))) (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) p)) (@field_at CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) (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 p (@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 => @andp mpred Nveric (@prop mpred Nveric (@eq (list val) (@app val contents (@cons val p (@nil val))) (@app val prefix (@cons val tl (@nil val))))) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@lseg CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh Ews prefix hd tl) (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) tl)) (@field_at CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) nullval tl)))))) *)
  + subst. Exists (p,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 p p) q) (@malloc_token CompSpecs Ews t_struct_fifo q)) (@andp mpred Nveric (@prop mpred Nveric (and (@eq val nullval v) (not (ptr_eq nullval 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)) (@emp mpred Nveric Sveric)) (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@vund CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) nullval)) (@field_at CompSpecs Ews (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _next) (@nil gfield)) (@valinject CompSpecs (@nested_field_type CompSpecs (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _next) (@nil gfield))) y) nullval)) (@lseg CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh Ews prefix y tl))))) (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) tl)) (@field_at CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) nullval tl)) (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) p)) (@field_at CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) (Vint (Int.repr Z0)) p)) (@exp mpred Nveric (prod val val) (fun ht : prod val val => let (hd, tl0) := 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 tl0))) (@data_at CompSpecs Ews t_struct_fifo (@pair val val hd tl0) q)) (@malloc_token CompSpecs Ews t_struct_fifo q)) (if @isnil val (@app val (@app val (@cons val v prefix) (@cons val tl (@nil val))) (@cons val p (@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 => @andp mpred Nveric (@prop mpred Nveric (@eq (list val) (@app val (@app val (@cons val v prefix) (@cons val tl (@nil val))) (@cons val p (@nil val))) (@app val prefix0 (@cons val tl0 (@nil val))))) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@lseg CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh Ews prefix0 hd tl0) (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) tl0)) (@field_at CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) nullval tl0)))))) *)
     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))) (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) p)) (@field_at CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) (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 => @andp mpred Nveric (@prop mpred Nveric (@eq (list val) (@cons val p (@nil val)) (@app val prefix (@cons val p (@nil val))))) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@lseg CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh Ews prefix p p) (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) p)) (@field_at CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) nullval p))))) *)
     Exists (@nil val).
(* Goal: False *)
      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 (prod val val) (Vint a0) (@pair val val (Vint b0) Vundef)) p)) (@andp mpred Nveric (@prop mpred Nveric (@eq val p p)) (@sepcon mpred Nveric Sveric (mem_mgr gv) (@sepcon mpred Nveric Sveric (@field_at CompSpecs Qsh' (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _a) (@nil gfield)) (Vint a0) p) (@sepcon mpred Nveric Sveric (@field_at CompSpecs Qsh' (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _b) (@nil gfield)) (Vint b0) p) (@sepcon mpred Nveric Sveric (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) p) (@sepcon mpred Nveric Sveric (@field_at_ CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) p) (@malloc_token CompSpecs Ews t_struct_elem p))))))) *)
      entailer!.
   + Intros prefix.
      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 (prod val val) (Vint a0) (@pair val val (Vint b0) Vundef)) p)) (@andp mpred Nveric (@prop mpred Nveric (@eq val p p)) (@sepcon mpred Nveric Sveric (mem_mgr gv) (@sepcon mpred Nveric Sveric (@field_at CompSpecs Qsh' (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _a) (@nil gfield)) (Vint a0) p) (@sepcon mpred Nveric Sveric (@field_at CompSpecs Qsh' (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _b) (@nil gfield)) (Vint b0) p) (@sepcon mpred Nveric Sveric (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) p) (@sepcon mpred Nveric Sveric (@field_at_ CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) p) (@malloc_token CompSpecs Ews t_struct_elem 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 (@data_at CompSpecs Ews t_struct_fifo (@pair val val p p) q) (@malloc_token CompSpecs Ews t_struct_fifo q)) (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) nullval)) (@field_at CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) nullval nullval)) (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) p)) (@field_at CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) (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 (@app val (@nil val) (@cons val nullval (@nil val))) (@cons val p (@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 => @andp mpred Nveric (@prop mpred Nveric (@eq (list val) (@app val (@app val (@nil val) (@cons val nullval (@nil val))) (@cons val p (@nil val))) (@app val prefix (@cons val tl (@nil val))))) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@lseg CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh Ews prefix hd tl) (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) tl)) (@field_at CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) nullval 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 (@data_at CompSpecs Ews t_struct_fifo (@pair val val p p) q) (@malloc_token CompSpecs Ews t_struct_fifo q)) (@lseg CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh Ews (@cons val v prefix) nullval tl)) (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) tl)) (@field_at CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) nullval tl)) (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) p)) (@field_at CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) (Vint (Int.repr Z0)) p)) (@exp mpred Nveric (prod val val) (fun ht : prod val val => let (hd, tl0) := 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 tl0))) (@data_at CompSpecs Ews t_struct_fifo (@pair val val hd tl0) q)) (@malloc_token CompSpecs Ews t_struct_fifo q)) (if @isnil val (@app val (@app val (@cons val v prefix) (@cons val tl (@nil val))) (@cons val p (@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 => @andp mpred Nveric (@prop mpred Nveric (@eq (list val) (@app val (@app val (@cons val v prefix) (@cons val tl (@nil val))) (@cons val p (@nil val))) (@app val prefix0 (@cons val tl0 (@nil val))))) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@lseg CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh Ews prefix0 hd tl0) (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) tl0)) (@field_at CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) nullval tl0)))))) *)
      contradiction (field_compatible_isptr _ _ _ H7).
(* 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 (and (@eq val nullval v) (not (ptr_eq nullval 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)) (@emp mpred Nveric Sveric)) (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@vund CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) nullval)) (@field_at CompSpecs Ews (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _next) (@nil gfield)) (@valinject CompSpecs (@nested_field_type CompSpecs (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _next) (@nil gfield))) y) nullval)) (@lseg CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh Ews prefix y tl))))) (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) tl)) (@field_at CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) nullval tl)) (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) p)) (@field_at CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) (Vint (Int.repr Z0)) p)) (@exp mpred Nveric (prod val val) (fun ht : prod val val => let (hd, tl0) := 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 tl0))) (@data_at CompSpecs Ews t_struct_fifo (@pair val val hd tl0) q)) (@malloc_token CompSpecs Ews t_struct_fifo q)) (if @isnil val (@app val (@app val (@cons val v prefix) (@cons val tl (@nil val))) (@cons val p (@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 => @andp mpred Nveric (@prop mpred Nveric (@eq (list val) (@app val (@app val (@cons val v prefix) (@cons val tl (@nil val))) (@cons val p (@nil val))) (@app val prefix0 (@cons val tl0 (@nil val))))) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@lseg CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh Ews prefix0 hd tl0) (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) tl0)) (@field_at CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) nullval tl0)))))) *)
      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 (and (@eq val nullval v) (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)) (@emp mpred Nveric Sveric)) (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@vund CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) nullval)) (@field_at CompSpecs Ews (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _next) (@nil gfield)) y nullval)) (@lseg CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh Ews prefix y tl))))) (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) tl)) (@field_at CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) nullval tl)) (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) p)) (@field_at CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) (Vint (Int.repr Z0)) p)) (@exp mpred Nveric (prod val val) (fun ht : prod val val => let (hd, tl0) := 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 tl0))) (@data_at CompSpecs Ews t_struct_fifo (@pair val val hd tl0) q)) (@malloc_token CompSpecs Ews t_struct_fifo q)) (if @isnil val (@cons val v (@app val (@app val prefix (@cons val tl (@nil val))) (@cons val p (@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 => @andp mpred Nveric (@prop mpred Nveric (@eq (list val) (@cons val v (@app val (@app val prefix (@cons val tl (@nil val))) (@cons val p (@nil val)))) (@app val prefix0 (@cons val tl0 (@nil val))))) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@lseg CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh Ews prefix0 hd tl0) (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) tl0)) (@field_at CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) nullval tl0)))))) *)
      Intros y. saturate_local.
(* 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)) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@emp mpred Nveric Sveric) (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@vund CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) nullval)) (@field_at CompSpecs Ews (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _next) (@nil gfield)) y nullval)) (@lseg CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh Ews prefix y tl))) (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) tl)) (@field_at CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) nullval tl)) (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) p)) (@field_at CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) (Vint (Int.repr Z0)) p)) (@exp mpred Nveric (prod val val) (fun ht : prod val val => let (hd, tl0) := 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 tl0))) (@data_at CompSpecs Ews t_struct_fifo (@pair val val hd tl0) q)) (@malloc_token CompSpecs Ews t_struct_fifo q)) (if @isnil val (@cons val v (@app val (@app val prefix (@cons val tl (@nil val))) (@cons val p (@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 => @andp mpred Nveric (@prop mpred Nveric (@eq (list val) (@cons val v (@app val (@app val prefix (@cons val tl (@nil val))) (@cons val p (@nil val)))) (@app val prefix0 (@cons val tl0 (@nil val))))) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@lseg CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh Ews prefix0 hd tl0) (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) tl0)) (@field_at CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) nullval tl0)))))) *)
      contradiction (field_compatible_isptr _ _ _ H11).
* (* 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 (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) p) (@cons mpred (@field_at CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) (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 => @andp mpred Nveric (@prop mpred Nveric (@eq (list val) contents (@app val prefix (@cons val tl (@nil val))))) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@lseg CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh Ews prefix hd tl) (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) tl)) (@field_at CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) nullval tl)))) (@cons mpred (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) p) (@cons mpred (@field_at CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) (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).
(* Goal: False *)
  + Intros. contradiction H; auto.
  + Intros prefix.
     forward. (*  t->next=p; *)
  (* goal 12 *)
     forward. (* Q->tail=p; *)
  (* goal 13 *)
(* 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 (prod val val) (Vint a0) (@pair val val (Vint b0) Vundef)) p)) (@andp mpred Nveric (@prop mpred Nveric (@eq val p p)) (@sepcon mpred Nveric Sveric (mem_mgr gv) (@sepcon mpred Nveric Sveric (@field_at CompSpecs Qsh' (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _a) (@nil gfield)) (Vint a0) p) (@sepcon mpred Nveric Sveric (@field_at CompSpecs Qsh' (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _b) (@nil gfield)) (Vint b0) p) (@sepcon mpred Nveric Sveric (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) p) (@sepcon mpred Nveric Sveric (@field_at_ CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) p) (@malloc_token CompSpecs Ews t_struct_elem 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 x tl) q) (@malloc_token CompSpecs Ews t_struct_fifo q)) (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@vund CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) v)) (@field_at CompSpecs Ews (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _next) (@nil gfield)) x v)) (@lseg CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh Ews prefix x tl)) (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) tl)) (@field_at CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) nullval tl)) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (fifo (@app val prefix (@cons val tl (@nil val))) q) (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) v)) (@field_at_ CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) v)) *)
     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) (_ : val) => @emp mpred Nveric Sveric) QS Qsh Ews prefix hd tl)) (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) tl)) (@field_at CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) p tl)) (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) p)) (@field_at CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) (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 tl (@nil val))) (@cons val p (@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 => @andp mpred Nveric (@prop mpred Nveric (@eq (list val) (@app val (@app val prefix (@cons val tl (@nil val))) (@cons val p (@nil val))) (@app val prefix0 (@cons val p (@nil val))))) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@lseg CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh Ews prefix0 hd p) (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) p)) (@field_at CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) nullval p))))) *)
     rewrite if_false by (clear; destruct prefix; simpl; congruence).
     Exists  (prefix ++ tl :: nil).
(* 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) (_ : val) => @emp mpred Nveric Sveric) QS Qsh Ews prefix hd tl)) (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) tl)) (@field_at CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) p tl)) (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) p)) (@field_at CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) (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 tl (@nil val))) (@cons val p (@nil val))) (@app val (@app val prefix (@cons val tl (@nil val))) (@cons val p (@nil val))))) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@lseg CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh Ews (@app val prefix (@cons val tl (@nil val))) hd p) (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) p)) (@field_at CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) nullval p)))) *)
     entailer.
     match goal with
     | |- _ |-- _ * _ * ?AA => remember AA as A
     end.     (* prevent it from canceling! *)
(* 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) (_ : val) => @emp mpred Nveric Sveric) QS Qsh Ews prefix hd tl)) (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) tl)) (@field_at CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) p tl)) (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) p)) (@field_at CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) (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) (_ : val) => @emp mpred Nveric Sveric) QS Qsh Ews (@app val prefix (@cons val tl (@nil val))) hd p)) (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) p)) A) *)
     simpl sizeof.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@lseg CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh Ews prefix hd tl) (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) tl)) (@field_at CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) p tl)) (@field_at CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) (Vint (Int.repr Z0)) p)) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@emp mpred Nveric Sveric) (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) tl)) (@field_at CompSpecs Ews (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _next) (@nil gfield)) (@valinject CompSpecs (@nested_field_type CompSpecs (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _next) (@nil gfield))) p) tl)) (@lseg CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh Ews prefix hd tl)) (@field_at CompSpecs Ews (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _next) (@nil gfield)) (@valinject CompSpecs (@nested_field_type CompSpecs (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _next) (@nil gfield))) (Vint Int.zero)) p)) *)
     cancel. subst A.
     eapply derives_trans; [ |
       apply (lseg_cons_right_neq _ _ _ _ _ ((Vundef,Vundef) : elemtype QS));
        auto ].
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@lseg CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh Ews prefix hd tl) (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) tl)) (@field_at CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) p tl)) (@field_at CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) (Vint (Int.repr Z0)) p)) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@emp mpred Nveric Sveric) (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) tl)) (@field_at CompSpecs Ews (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _next) (@nil gfield)) (@valinject CompSpecs (@nested_field_type CompSpecs (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _next) (@nil gfield))) p) tl)) (@lseg CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh Ews prefix hd tl)) (@field_at CompSpecs Ews (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _next) (@nil gfield)) (@valinject CompSpecs (@nested_field_type CompSpecs (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _next) (@nil gfield))) (Vint Int.zero)) p)) *)
     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 p 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, fifo_body 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 p 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 => @andp mpred Nveric (@prop mpred Nveric (@eq (list val) (@cons val p contents) (@app val prefix (@cons val tl (@nil val))))) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@lseg CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh Ews prefix hd tl) (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) tl)) (@field_at CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) 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 => @andp mpred Nveric (@prop mpred Nveric (@eq (list val) (@cons val p contents) (@app val prefix (@cons val tl (@nil val))))) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@lseg CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh Ews prefix hd tl) (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) tl)) (@field_at CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) 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.
forward.  (*   p = 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) (_ : val) => @emp mpred Nveric Sveric) QS Qsh Ews prefix hd tl) (@cons mpred (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) tl) (@cons mpred (@field_at CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) 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.
+ subst_any.
(* Goal: False *)
   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 (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) tl) (@cons mpred (@field_at CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) 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 (@emp mpred Nveric Sveric) (@cons mpred (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@vund CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) hd) (@cons mpred (@field_at CompSpecs Ews (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _next) (@nil gfield)) x hd) (@cons mpred (@lseg CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh Ews prefix x tl) (@cons mpred (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) tl) (@cons mpred (@field_at CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) 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 (@data_at CompSpecs Ews t_struct_fifo (@pair val val x tl) q) (@malloc_token CompSpecs Ews t_struct_fifo q)) (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@vund CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) v)) (@field_at CompSpecs Ews (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _next) (@nil gfield)) x v)) (@lseg CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh Ews prefix x tl)) (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) tl)) (@field_at CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) nullval tl)) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (fifo (@app val prefix (@cons val tl (@nil val))) q) (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) v)) (@field_at_ CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) v)) *)
   unfold fifo, fifo_body. Exists (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 (prod val val) (Vint a0) (@pair val val (Vint b0) Vundef)) p)) (@andp mpred Nveric (@prop mpred Nveric (@eq val p p)) (@sepcon mpred Nveric Sveric (mem_mgr gv) (@sepcon mpred Nveric Sveric (@field_at CompSpecs Qsh' (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _a) (@nil gfield)) (Vint a0) p) (@sepcon mpred Nveric Sveric (@field_at CompSpecs Qsh' (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _b) (@nil gfield)) (Vint b0) p) (@sepcon mpred Nveric Sveric (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) p) (@sepcon mpred Nveric Sveric (@field_at_ CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) p) (@malloc_token CompSpecs Ews t_struct_elem p))))))) *)
   simpl sizeof; entailer!.
(* Goal: False *)
+ 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 (and (@eq val hd v) (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)) (@emp mpred Nveric Sveric)) (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@vund CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) hd)) (@field_at CompSpecs Ews (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _next) (@nil gfield)) (@valinject CompSpecs (@nested_field_type CompSpecs (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _next) (@nil gfield))) y) hd)) (@lseg CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh Ews prefix y tl)))) (@cons mpred (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) tl) (@cons mpred (@field_at CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) 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 (@emp mpred Nveric Sveric) (@cons mpred (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@vund CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) hd) (@cons mpred (@field_at CompSpecs Ews (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _next) (@nil gfield)) x hd) (@cons mpred (@lseg CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh Ews prefix x tl) (@cons mpred (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) tl) (@cons mpred (@field_at CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) 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 (@data_at CompSpecs Ews t_struct_fifo (@pair val val x tl) q) (@malloc_token CompSpecs Ews t_struct_fifo q)) (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@vund CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) v)) (@field_at CompSpecs Ews (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _next) (@nil gfield)) x v)) (@lseg CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh Ews prefix x tl)) (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) tl)) (@field_at CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) nullval tl)) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (fifo (@app val prefix (@cons val tl (@nil val))) q) (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) v)) (@field_at_ CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) v)) *)
    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 (@data_at CompSpecs Ews t_struct_fifo (@pair val val x tl) q) (@malloc_token CompSpecs Ews t_struct_fifo q)) (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@vund CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) v)) (@field_at CompSpecs Ews (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _next) (@nil gfield)) x v)) (@lseg CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh Ews prefix x tl)) (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) tl)) (@field_at CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) nullval tl)) (@sepcon mpred Nveric Sveric (@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 tl (@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 => @andp mpred Nveric (@prop mpred Nveric (@eq (list val) (@app val prefix (@cons val tl (@nil val))) (@app val prefix0 (@cons val tl (@nil val))))) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@lseg CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh Ews prefix0 x tl) (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) tl)) (@field_at CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) nullval tl))))) (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) v)) (@field_at_ CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) v)) *)
    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 (@data_at CompSpecs Ews t_struct_fifo (@pair val val x tl) q) (@malloc_token CompSpecs Ews t_struct_fifo q)) (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@vund CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) v)) (@field_at CompSpecs Ews (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _next) (@nil gfield)) x v)) (@lseg CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh Ews prefix x tl)) (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) tl)) (@field_at CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) nullval tl)) (@sepcon mpred Nveric Sveric (@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 => @andp mpred Nveric (@prop mpred Nveric (@eq (list val) (@app val prefix (@cons val tl (@nil val))) (@app val prefix0 (@cons val tl (@nil val))))) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@lseg CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh Ews prefix0 x tl) (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) tl)) (@field_at CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) nullval tl))))) (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) v)) (@field_at_ CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) v)) *)
    Exists 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 (prod val val) (Vint a0) (@pair val val (Vint b0) Vundef)) p)) (@andp mpred Nveric (@prop mpred Nveric (@eq val p p)) (@sepcon mpred Nveric Sveric (mem_mgr gv) (@sepcon mpred Nveric Sveric (@field_at CompSpecs Qsh' (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _a) (@nil gfield)) (Vint a0) p) (@sepcon mpred Nveric Sveric (@field_at CompSpecs Qsh' (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _b) (@nil gfield)) (Vint b0) p) (@sepcon mpred Nveric Sveric (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) p) (@sepcon mpred Nveric Sveric (@field_at_ CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) p) (@malloc_token CompSpecs Ews t_struct_elem p))))))) *)
    entailer!.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@field_at CompSpecs Qsh' t_struct_elem (@cons gfield (StructField _a) (@nil gfield)) (Vint a0) p) (@field_at CompSpecs Qsh' t_struct_elem (@cons gfield (StructField _b) (@nil gfield)) (Vint b0) p)) (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) p)) (@field_at_ CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) p)) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@field_at CompSpecs Qsh' (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _a) (@nil gfield)) (Vint a0) p) (@field_at CompSpecs Qsh' (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _b) (@nil gfield)) (Vint b0) p)) (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) p)) (@field_at_ CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) p)) *)
    apply derives_refl.
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. rename a into a0; rename b into b0.
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 _a (Vint a0)) (@cons localdef (temp _b (Vint b0)) (@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)) _a tint) (Etempvar _a 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 _a (Vint a0)) (@cons localdef (temp _b (Vint b0)) (@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)) _a tint) (Etempvar _a tint)) MORE_COMMANDS) POSTCONDITION *)
 Intros p.
  forward.  (*  p->a=a; *)
  progress simpl.  (* this should not be necessary -- Qinxiang, please look *)
  forward.  (*  p->b=b; *)
  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 (prod val val) (Vint a0) (@pair val val (Vint b0) 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 (@field_at CompSpecs Qsh' (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _a) (@nil gfield)) (Vint a0) a) (@sepcon mpred Nveric Sveric (@field_at CompSpecs Qsh' (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _b) (@nil gfield)) (Vint b0) a) (@sepcon mpred Nveric Sveric (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) a) (@sepcon mpred Nveric Sveric (@field_at_ CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) a) (@malloc_token CompSpecs Ews t_struct_elem 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 (prod val val) (Vint a0) (@pair val val (Vint b0) Vundef)) p)) (@andp mpred Nveric (@prop mpred Nveric (@eq val p p)) (@sepcon mpred Nveric Sveric (mem_mgr gv) (@sepcon mpred Nveric Sveric (@field_at CompSpecs Qsh' (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _a) (@nil gfield)) (Vint a0) p) (@sepcon mpred Nveric Sveric (@field_at CompSpecs Qsh' (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _b) (@nil gfield)) (Vint b0) p) (@sepcon mpred Nveric Sveric (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) p) (@sepcon mpred Nveric Sveric (@field_at_ CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) p) (@malloc_token CompSpecs Ews t_struct_elem p))))))) *)
  entailer!.
(* Goal: @derives mpred Nveric (@data_at CompSpecs Ews t_struct_elem (@pair val (prod val val) (Vint a0) (@pair val val (Vint b0) Vundef)) p) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@field_at CompSpecs Qsh' (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _a) (@nil gfield)) (Vint a0) p) (@field_at CompSpecs Qsh' (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _b) (@nil gfield)) (Vint b0) p)) (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) p)) (@field_at_ CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) p)) *)
  rewrite make_unmake.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@field_at CompSpecs Qsh' t_struct_elem (@cons gfield (StructField _a) (@nil gfield)) (Vint a0) p) (@field_at CompSpecs Qsh' t_struct_elem (@cons gfield (StructField _b) (@nil gfield)) (Vint b0) p)) (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) p)) (@field_at_ CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) p)) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@field_at CompSpecs Qsh' (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _a) (@nil gfield)) (Vint a0) p) (@field_at CompSpecs Qsh' (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _b) (@nil gfield)) (Vint b0) p)) (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) p)) (@field_at_ CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) p)) *)
  apply derives_refl.
Qed.

Hint Resolve readable_share_Qsh'.

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,10); *)
     (Int.repr 1, Int.repr 10, gv).
Intros p'.
forward_call (* fifo_put(Q,p);*)
    ((q, @nil val),p').

forward_call  (*  p = make_elem(2,20); *)
     (Int.repr 2, Int.repr 20, gv).
Intros p2.
simpl app.
 forward_call  (* fifo_put(Q,p); *)
    ((q,(p':: nil)),p2).
simpl app.
forward_call  (*   p' = fifo_get(Q); p = p'; *)
    ((q,(p2 :: nil)),p').
forward. (*   i = p->a;  *)
forward. (*   j = p->b; *)
forward_call (*  free(p, sizeof( *p)); *)
   (t_struct_elem, p', gv).
(* 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)) *)
{
 assert_PROP (isptr p'); [entailer! | rewrite if_false by (intro; subst; contradiction) ].
 sep_apply (eq_sym (make_unmake (Int.repr 1) (Int.repr 10) p')).
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@lseg CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh Ews prefix hd tl) (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) tl)) (@field_at CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) p tl)) (@field_at CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) (Vint (Int.repr Z0)) p)) (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@emp mpred Nveric Sveric) (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) tl)) (@field_at CompSpecs Ews (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _next) (@nil gfield)) (@valinject CompSpecs (@nested_field_type CompSpecs (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _next) (@nil gfield))) p) tl)) (@lseg CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh Ews prefix hd tl)) (@field_at CompSpecs Ews (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _next) (@nil gfield)) (@valinject CompSpecs (@nested_field_type CompSpecs (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _next) (@nil gfield))) (Vint Int.zero)) p)) *)
 cancel.
}
forward. (* return i+j; *)
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 val (list val)) val) (fun x : prod (prod val (list val)) val => let (p0, p) := x in let (q, contents) := p0 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 (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) p) (@cons mpred (@field_at_ CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) p) (@nil mpred))))))) (fun x : prod (prod val (list val)) val => let (p0, p) := x in let (q, contents) := p0 in PROPx (@nil Prop) (LOCALx (@nil localdef) (SEPx (@cons mpred (fifo (@app val contents (@cons val p (@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 (p0, p) := x in let (q, contents) := p0 in PROPx (@nil Prop) (LOCALx (@cons localdef (temp _Q q) (@nil localdef)) (SEPx (@cons mpred (fifo (@cons val p contents) q) (@nil mpred))))) (fun x : prod (prod val (list val)) val => let (p0, p) := x in let (q, contents) := p0 in PROPx (@nil Prop) (LOCALx (@cons localdef (temp ret_temp p) (@nil localdef)) (SEPx (@cons mpred (fifo contents q) (@cons mpred (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) p) (@cons mpred (@field_at_ CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) p) (@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 _a tint) (@cons (prod ident type) (@pair ident type _b tint) (@nil (prod ident type)))) (tptr t_struct_elem)) cc_default (prod (prod Int.int Int.int) globals) (fun x : prod (prod Int.int Int.int) globals => let (p, gv) := x in let (a, b) := p in PROPx (@nil Prop) (LOCALx (@cons localdef (temp _a (Vint a)) (@cons localdef (temp _b (Vint b)) (@cons localdef (gvars gv) (@nil localdef)))) (SEPx (@cons mpred (mem_mgr gv) (@nil mpred))))) (fun x : prod (prod Int.int Int.int) globals => let (p, gv) := x in let (a, b) := 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 (mem_mgr gv) (@cons mpred (@field_at CompSpecs Qsh' (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _a) (@nil gfield)) (Vint a) p0) (@cons mpred (@field_at CompSpecs Qsh' (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _b) (@nil gfield)) (Vint b) p0) (@cons mpred (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) p0) (@cons mpred (@field_at_ CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) p0) (@cons mpred (@malloc_token CompSpecs Ews t_struct_elem p0) (@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 (Z.add (Zpos xH) (Zpos (xO (xI (xO 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 val (list val)) val) (fun x : prod (prod val (list val)) val => let (p0, p) := x in let (q, contents) := p0 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 (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) p) (@cons mpred (@field_at_ CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) p) (@nil mpred))))))) (fun x : prod (prod val (list val)) val => let (p0, p) := x in let (q, contents) := p0 in PROPx (@nil Prop) (LOCALx (@nil localdef) (SEPx (@cons mpred (fifo (@app val contents (@cons val p (@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 (p0, p) := x in let (q, contents) := p0 in PROPx (@nil Prop) (LOCALx (@cons localdef (temp _Q q) (@nil localdef)) (SEPx (@cons mpred (fifo (@cons val p contents) q) (@nil mpred))))) (fun x : prod (prod val (list val)) val => let (p0, p) := x in let (q, contents) := p0 in PROPx (@nil Prop) (LOCALx (@cons localdef (temp ret_temp p) (@nil localdef)) (SEPx (@cons mpred (fifo contents q) (@cons mpred (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) p) (@cons mpred (@field_at_ CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) p) (@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 _a tint) (@cons (prod ident type) (@pair ident type _b tint) (@nil (prod ident type)))) (tptr t_struct_elem)) cc_default (prod (prod Int.int Int.int) globals) (fun x : prod (prod Int.int Int.int) globals => let (p, gv) := x in let (a, b) := p in PROPx (@nil Prop) (LOCALx (@cons localdef (temp _a (Vint a)) (@cons localdef (temp _b (Vint b)) (@cons localdef (gvars gv) (@nil localdef)))) (SEPx (@cons mpred (mem_mgr gv) (@nil mpred))))) (fun x : prod (prod Int.int Int.int) globals => let (p, gv) := x in let (a, b) := 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 (mem_mgr gv) (@cons mpred (@field_at CompSpecs Qsh' (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _a) (@nil gfield)) (Vint a) p0) (@cons mpred (@field_at CompSpecs Qsh' (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _b) (@nil gfield)) (Vint b) p0) (@cons mpred (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) p0) (@cons mpred (@field_at_ CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) p0) (@cons mpred (@malloc_token CompSpecs Ews t_struct_elem p0) (@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 (Z.add (Zpos xH) (Zpos (xO (xI (xO 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 val (list val)) val) (fun x : prod (prod val (list val)) val => let (p0, p) := x in let (q, contents) := p0 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 (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) p) (@cons mpred (@field_at_ CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) p) (@nil mpred))))))) (fun x : prod (prod val (list val)) val => let (p0, p) := x in let (q, contents) := p0 in PROPx (@nil Prop) (LOCALx (@nil localdef) (SEPx (@cons mpred (fifo (@app val contents (@cons val p (@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 (p0, p) := x in let (q, contents) := p0 in PROPx (@nil Prop) (LOCALx (@cons localdef (temp _Q q) (@nil localdef)) (SEPx (@cons mpred (fifo (@cons val p contents) q) (@nil mpred))))) (fun x : prod (prod val (list val)) val => let (p0, p) := x in let (q, contents) := p0 in PROPx (@nil Prop) (LOCALx (@cons localdef (temp ret_temp p) (@nil localdef)) (SEPx (@cons mpred (fifo contents q) (@cons mpred (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) p) (@cons mpred (@field_at_ CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) p) (@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 _a tint) (@cons (prod ident type) (@pair ident type _b tint) (@nil (prod ident type)))) (tptr t_struct_elem)) cc_default (prod (prod Int.int Int.int) globals) (fun x : prod (prod Int.int Int.int) globals => let (p, gv) := x in let (a, b) := p in PROPx (@nil Prop) (LOCALx (@cons localdef (temp _a (Vint a)) (@cons localdef (temp _b (Vint b)) (@cons localdef (gvars gv) (@nil localdef)))) (SEPx (@cons mpred (mem_mgr gv) (@nil mpred))))) (fun x : prod (prod Int.int Int.int) globals => let (p, gv) := x in let (a, b) := 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 (mem_mgr gv) (@cons mpred (@field_at CompSpecs Qsh' (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _a) (@nil gfield)) (Vint a) p0) (@cons mpred (@field_at CompSpecs Qsh' (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _b) (@nil gfield)) (Vint b) p0) (@cons mpred (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) p0) (@cons mpred (@field_at_ CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) p0) (@cons mpred (@malloc_token CompSpecs Ews t_struct_elem p0) (@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 (Z.add (Zpos xH) (Zpos (xO (xI (xO 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 val (list val)) val) (fun x : prod (prod val (list val)) val => let (p0, p) := x in let (q, contents) := p0 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 (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) p) (@cons mpred (@field_at_ CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) p) (@nil mpred))))))) (fun x : prod (prod val (list val)) val => let (p0, p) := x in let (q, contents) := p0 in PROPx (@nil Prop) (LOCALx (@nil localdef) (SEPx (@cons mpred (fifo (@app val contents (@cons val p (@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 (p0, p) := x in let (q, contents) := p0 in PROPx (@nil Prop) (LOCALx (@cons localdef (temp _Q q) (@nil localdef)) (SEPx (@cons mpred (fifo (@cons val p contents) q) (@nil mpred))))) (fun x : prod (prod val (list val)) val => let (p0, p) := x in let (q, contents) := p0 in PROPx (@nil Prop) (LOCALx (@cons localdef (temp ret_temp p) (@nil localdef)) (SEPx (@cons mpred (fifo contents q) (@cons mpred (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) p) (@cons mpred (@field_at_ CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) p) (@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 _a tint) (@cons (prod ident type) (@pair ident type _b tint) (@nil (prod ident type)))) (tptr t_struct_elem)) cc_default (prod (prod Int.int Int.int) globals) (fun x : prod (prod Int.int Int.int) globals => let (p, gv) := x in let (a, b) := p in PROPx (@nil Prop) (LOCALx (@cons localdef (temp _a (Vint a)) (@cons localdef (temp _b (Vint b)) (@cons localdef (gvars gv) (@nil localdef)))) (SEPx (@cons mpred (mem_mgr gv) (@nil mpred))))) (fun x : prod (prod Int.int Int.int) globals => let (p, gv) := x in let (a, b) := 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 (mem_mgr gv) (@cons mpred (@field_at CompSpecs Qsh' (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _a) (@nil gfield)) (Vint a) p0) (@cons mpred (@field_at CompSpecs Qsh' (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _b) (@nil gfield)) (Vint b) p0) (@cons mpred (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) p0) (@cons mpred (@field_at_ CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) p0) (@cons mpred (@malloc_token CompSpecs Ews t_struct_elem p0) (@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 (Z.add (Zpos xH) (Zpos (xO (xI (xO 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 val (list val)) val) (fun x : prod (prod val (list val)) val => let (p0, p) := x in let (q, contents) := p0 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 (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) p) (@cons mpred (@field_at_ CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) p) (@nil mpred))))))) (fun x : prod (prod val (list val)) val => let (p0, p) := x in let (q, contents) := p0 in PROPx (@nil Prop) (LOCALx (@nil localdef) (SEPx (@cons mpred (fifo (@app val contents (@cons val p (@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 (p0, p) := x in let (q, contents) := p0 in PROPx (@nil Prop) (LOCALx (@cons localdef (temp _Q q) (@nil localdef)) (SEPx (@cons mpred (fifo (@cons val p contents) q) (@nil mpred))))) (fun x : prod (prod val (list val)) val => let (p0, p) := x in let (q, contents) := p0 in PROPx (@nil Prop) (LOCALx (@cons localdef (temp ret_temp p) (@nil localdef)) (SEPx (@cons mpred (fifo contents q) (@cons mpred (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) p) (@cons mpred (@field_at_ CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) p) (@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 _a tint) (@cons (prod ident type) (@pair ident type _b tint) (@nil (prod ident type)))) (tptr t_struct_elem)) cc_default (prod (prod Int.int Int.int) globals) (fun x : prod (prod Int.int Int.int) globals => let (p, gv) := x in let (a, b) := p in PROPx (@nil Prop) (LOCALx (@cons localdef (temp _a (Vint a)) (@cons localdef (temp _b (Vint b)) (@cons localdef (gvars gv) (@nil localdef)))) (SEPx (@cons mpred (mem_mgr gv) (@nil mpred))))) (fun x : prod (prod Int.int Int.int) globals => let (p, gv) := x in let (a, b) := 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 (mem_mgr gv) (@cons mpred (@field_at CompSpecs Qsh' (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _a) (@nil gfield)) (Vint a) p0) (@cons mpred (@field_at CompSpecs Qsh' (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _b) (@nil gfield)) (Vint b) p0) (@cons mpred (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) p0) (@cons mpred (@field_at_ CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) p0) (@cons mpred (@malloc_token CompSpecs Ews t_struct_elem p0) (@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 (Z.add (Zpos xH) (Zpos (xO (xI (xO 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 val (list val)) val) (fun x : prod (prod val (list val)) val => let (p0, p) := x in let (q, contents) := p0 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 (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) p) (@cons mpred (@field_at_ CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) p) (@nil mpred))))))) (fun x : prod (prod val (list val)) val => let (p0, p) := x in let (q, contents) := p0 in PROPx (@nil Prop) (LOCALx (@nil localdef) (SEPx (@cons mpred (fifo (@app val contents (@cons val p (@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 (p0, p) := x in let (q, contents) := p0 in PROPx (@nil Prop) (LOCALx (@cons localdef (temp _Q q) (@nil localdef)) (SEPx (@cons mpred (fifo (@cons val p contents) q) (@nil mpred))))) (fun x : prod (prod val (list val)) val => let (p0, p) := x in let (q, contents) := p0 in PROPx (@nil Prop) (LOCALx (@cons localdef (temp ret_temp p) (@nil localdef)) (SEPx (@cons mpred (fifo contents q) (@cons mpred (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) p) (@cons mpred (@field_at_ CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) p) (@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 _a tint) (@cons (prod ident type) (@pair ident type _b tint) (@nil (prod ident type)))) (tptr t_struct_elem)) cc_default (prod (prod Int.int Int.int) globals) (fun x : prod (prod Int.int Int.int) globals => let (p, gv) := x in let (a, b) := p in PROPx (@nil Prop) (LOCALx (@cons localdef (temp _a (Vint a)) (@cons localdef (temp _b (Vint b)) (@cons localdef (gvars gv) (@nil localdef)))) (SEPx (@cons mpred (mem_mgr gv) (@nil mpred))))) (fun x : prod (prod Int.int Int.int) globals => let (p, gv) := x in let (a, b) := 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 (mem_mgr gv) (@cons mpred (@field_at CompSpecs Qsh' (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _a) (@nil gfield)) (Vint a) p0) (@cons mpred (@field_at CompSpecs Qsh' (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _b) (@nil gfield)) (Vint b) p0) (@cons mpred (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) p0) (@cons mpred (@field_at_ CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) p0) (@cons mpred (@malloc_token CompSpecs Ews t_struct_elem p0) (@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 (Z.add (Zpos xH) (Zpos (xO (xI (xO 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 (p0, p) := x in let (q, contents) := p0 in PROPx (@nil Prop) (LOCALx (@cons localdef (temp _Q q) (@nil localdef)) (SEPx (@cons mpred (fifo (@cons val p contents) q) (@nil mpred))))) (fun x : prod (prod val (list val)) val => let (p0, p) := x in let (q, contents) := p0 in PROPx (@nil Prop) (LOCALx (@cons localdef (temp ret_temp p) (@nil localdef)) (SEPx (@cons mpred (fifo contents q) (@cons mpred (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) p) (@cons mpred (@field_at_ CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) p) (@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 _a tint) (@cons (prod ident type) (@pair ident type _b tint) (@nil (prod ident type)))) (tptr t_struct_elem)) cc_default (prod (prod Int.int Int.int) globals) (fun x : prod (prod Int.int Int.int) globals => let (p, gv) := x in let (a, b) := p in PROPx (@nil Prop) (LOCALx (@cons localdef (temp _a (Vint a)) (@cons localdef (temp _b (Vint b)) (@cons localdef (gvars gv) (@nil localdef)))) (SEPx (@cons mpred (mem_mgr gv) (@nil mpred))))) (fun x : prod (prod Int.int Int.int) globals => let (p, gv) := x in let (a, b) := 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 (mem_mgr gv) (@cons mpred (@field_at CompSpecs Qsh' (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _a) (@nil gfield)) (Vint a) p0) (@cons mpred (@field_at CompSpecs Qsh' (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _b) (@nil gfield)) (Vint b) p0) (@cons mpred (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) p0) (@cons mpred (@field_at_ CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) p0) (@cons mpred (@malloc_token CompSpecs Ews t_struct_elem p0) (@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 (Z.add (Zpos xH) (Zpos (xO (xI (xO 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 (p0, p) := x in let (q, contents) := p0 in PROPx (@nil Prop) (LOCALx (@cons localdef (temp _Q q) (@nil localdef)) (SEPx (@cons mpred (fifo (@cons val p contents) q) (@nil mpred))))) (fun x : prod (prod val (list val)) val => let (p0, p) := x in let (q, contents) := p0 in PROPx (@nil Prop) (LOCALx (@cons localdef (temp ret_temp p) (@nil localdef)) (SEPx (@cons mpred (fifo contents q) (@cons mpred (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) p) (@cons mpred (@field_at_ CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) p) (@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 _a tint) (@cons (prod ident type) (@pair ident type _b tint) (@nil (prod ident type)))) (tptr t_struct_elem)) cc_default (prod (prod Int.int Int.int) globals) (fun x : prod (prod Int.int Int.int) globals => let (p, gv) := x in let (a, b) := p in PROPx (@nil Prop) (LOCALx (@cons localdef (temp _a (Vint a)) (@cons localdef (temp _b (Vint b)) (@cons localdef (gvars gv) (@nil localdef)))) (SEPx (@cons mpred (mem_mgr gv) (@nil mpred))))) (fun x : prod (prod Int.int Int.int) globals => let (p, gv) := x in let (a, b) := 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 (mem_mgr gv) (@cons mpred (@field_at CompSpecs Qsh' (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _a) (@nil gfield)) (Vint a) p0) (@cons mpred (@field_at CompSpecs Qsh' (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _b) (@nil gfield)) (Vint b) p0) (@cons mpred (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) p0) (@cons mpred (@field_at_ CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) p0) (@cons mpred (@malloc_token CompSpecs Ews t_struct_elem p0) (@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 (Z.add (Zpos xH) (Zpos (xO (xI (xO 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 _a tint) (@cons (prod ident type) (@pair ident type _b tint) (@nil (prod ident type)))) (tptr t_struct_elem)) cc_default (prod (prod Int.int Int.int) globals) (fun x : prod (prod Int.int Int.int) globals => let (p, gv) := x in let (a, b) := p in PROPx (@nil Prop) (LOCALx (@cons localdef (temp _a (Vint a)) (@cons localdef (temp _b (Vint b)) (@cons localdef (gvars gv) (@nil localdef)))) (SEPx (@cons mpred (mem_mgr gv) (@nil mpred))))) (fun x : prod (prod Int.int Int.int) globals => let (p, gv) := x in let (a, b) := 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 (mem_mgr gv) (@cons mpred (@field_at CompSpecs Qsh' (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _a) (@nil gfield)) (Vint a) p0) (@cons mpred (@field_at CompSpecs Qsh' (@list_struct CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS) (@cons gfield (StructField _b) (@nil gfield)) (Vint b) p0) (@cons mpred (@list_cell CompSpecs _elem _next (fun (_ : share) (_ : val) => @emp mpred Nveric Sveric) QS Qsh (@pair val val Vundef Vundef) p0) (@cons mpred (@field_at_ CompSpecs Ews t_struct_elem (@cons gfield (StructField _next) (@nil gfield)) p0) (@cons mpred (@malloc_token CompSpecs Ews t_struct_elem p0) (@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 (Z.add (Zpos xH) (Zpos (xO (xI (xO 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 (Z.add (Zpos xH) (Zpos (xO (xI (xO xH)))))))) (@nil localdef)) (SEPx (@cons mpred (@TT mpred Nveric) (@nil mpred))))))) (@nil (prod ident funspec))) *)
semax_func_cons body_main.
Qed.


