proposition: Lemma is_pointer_or_null_not_null: forall x, is_pointer_or_null x -> x <> nullval -> isptr x.
proof: Proof. intros. destruct x; try contradiction. hnf in H; subst i. contradiction H0; reflexivity. apply I. Qed.
imports: VST.floyd.proofauto CertiGraph.append.list_dt CertiGraph.append.append