fact: Definition spanning_spec := DECLARE _spanning WITH sh: wshare, g: Graph, x: pointer_val PRE [tptr (Tstruct _Node noattr)] PROP (vvalid g x; fst (fst (vgamma g x)) = false) PARAMS (pointer_val_val x) GLOBALS () SEP (graph sh x g) POST [ Tvoid ] EX g': Graph, PROP (spanning_tree g x g') LOCAL() SEP (vertices_at sh (reachable g x) g').
imports: CertiGraph.dispose.env_dispose_bin CertiGraph.graph.graph_model CertiGraph.graph.path_lemmas CertiGraph.graph.subgraph2 CertiGraph.graph.spanning_tree CertiGraph.graph.reachable_computable CertiGraph.msl_application.Graph CertiGraph.msl_application.GraphBin CertiGraph.msl_application.GraphBin_Mark CertiGraph.data_structure.spatial_graph_dispose_bin CertiGraph.data_structure.spatial_graph_unaligned_bin_VST CertiGraph.floyd_ext.share VST.msl.wand_frame VST.floyd.reassoc_seq VST.floyd.field_at_wand