fact: Definition concrete_valid_pointer (p: addr) := (!! (p = NullPointer) && emp) || data_at_ (Share.comp Ews) node_type (pointer_val_val p).
imports: CertiGraph.msl_ext.iter_sepcon CertiGraph.msl_application.Graph CertiGraph.msl_application.GraphBin VST.veric.SeparationLogic CertiGraph.copy.env_copy_bin