proposition: Lemma semax_lseg_nonnull (ls: listspec list_structid list_link list_token): forall (Espec: OracleKind) Delta P Q sh s v R c Post, ENTAIL Delta, PROPx P (LOCALx Q (SEPx (lseg ls sh s v nullval :: R))) |-- !!(typed_true (tptr list_struct) v) -> (forall (h: elemtype ls) (r: list (elemtype ls)) (y: val), s=h::r -> is_pointer_or_null y -> semax Delta (PROPx P (LOCALx Q (SEPx (list_token sh v :: list_cell ls sh h v :: field_at sh list_struct (StructField list_link :: nil) (valinject (nested_field_type list_struct (StructField list_link :: nil)) y) v :: lseg ls sh r y nullval :: R)))) c Post) -> semax Delta (PROPx P (LOCALx Q (SEPx (lseg ls sh s v nullval :: R)))) c Post.
proof: Proof. intros. assert_PROP (~ ptr_eq v nullval). eapply derives_trans; [apply H |]. normalize. apply semax_lseg_neq; auto. Qed.
imports: VST.floyd.base2 VST.floyd.client_lemmas VST.floyd.closed_lemmas VST.floyd.nested_pred_lemmas VST.floyd.nested_field_lemmas VST.floyd.efield_lemmas VST.floyd.mapsto_memory_block VST.floyd.reptype_lemmas VST.floyd.data_at_rec_lemmas VST.floyd.field_at VST.floyd.nested_loadstore VST.floyd.entailer