proposition: Lemma destruct_pointer_val_VP: forall x, pointer_val_val x <> nullval \/ isptr (pointer_val_val x) -> isptr (pointer_val_val x) /\ exists b i, x = ValidPointer b i.
proof: Proof. intros. destruct x; try simpl in H; try tauto. split; simpl; auto. exists b, i; auto. Qed.
imports: VST.floyd.base VST.floyd.canon VST.floyd.assert_lemmas VST.floyd.client_lemmas VST.floyd.reptype_lemmas VST.floyd.semax_tactics VST.floyd.local2ptree_denote VST.floyd.local2ptree_eval VST.floyd.call_lemmas VST.floyd.diagnosis VST.floyd.forward CertiGraph.lib.Coqlib CertiGraph.veric_ext.SeparationLogic CertiGraph.floyd_ext.ramification CertiGraph.floyd_ext.semax_ram_lemmas CertiGraph.floyd_ext.exists_trick CertiGraph.floyd_ext.closed_lemmas