fact: Definition makeSet_spec := DECLARE _makeSet WITH sh: wshare, g: UFGraph PRE [] PROP () PARAMS () GLOBALS () SEP (whole_graph sh g) POST [tptr (Tstruct _Node noattr)] EX g': UFGraph, EX rt: pointer_val, PROP (~ vvalid g rt ; vvalid g' rt ; is_partial_graph g g') LOCAL (temp ret_temp (pointer_val_val rt)) SEP (whole_graph sh g').
imports: CertiGraph.unionfind.env_unionfind CertiGraph.graph.graph_model CertiGraph.graph.path_lemmas CertiGraph.graph.subgraph2 CertiGraph.graph.graph_relation CertiGraph.graph.reachable_computable CertiGraph.msl_application.Graph CertiGraph.msl_application.UnionFindGraph CertiGraph.msl_application.GList CertiGraph.msl_application.GList_UnionFind CertiGraph.floyd_ext.share CertiGraph.unionfind.spatial_graph_glist