proposition: Lemma concrete_valid_pointer_null: concrete_valid_pointer null = emp.
proof: Proof. intros. unfold concrete_valid_pointer. apply pred_ext. + apply orp_left; [normalize |]. simpl pointer_val_val. saturate_local. destruct H; tauto. + apply orp_right1. normalize. Qed.
imports: CertiGraph.msl_ext.iter_sepcon CertiGraph.msl_application.Graph CertiGraph.msl_application.GraphBin VST.veric.SeparationLogic CertiGraph.copy.env_copy_bin