I am now working on proving the Lemma body_push in Verif_stack of VC:
Lemma body_push: semax_body Vprog Gprog f_push push_spec.https://softwarefoundations.cis.upenn.edu/vc-current/Verif_stack.html
But I’m stuck.
Here are my current proofs:
Lemma body_push: semax_body Vprog Gprog f_push push_spec.
Proof.
start_function.
forward_call (Tstruct _cons noattr, gv).
unfold stack. Intros vret q.
forward_if (PROP ( )
LOCAL (temp _q vret; gvars gv; temp _p p; temp _i (Vint (Int.repr i)))
SEP (mem_mgr gv;
if eq_dec vret nullval
then emp
else
malloc_token Ews (Tstruct _cons noattr) vret
* data_at_ Ews (Tstruct _cons noattr) vret;
malloc_token Ews (Tstruct _stack noattr) p;
data_at Ews (Tstruct _stack noattr) q p; listrep il q)).
+destruct vret;simpl;entailer!.
+
(* FILL IN HERE *) Admitted.