proposition: Lemma body_init_empty_graph: semax_body Vprog (@Gprog size) f_init_empty_graph init_empty_graph_spec.
proof: Proof. start_function. forward_call (gv, sh, sizeof t_wedgearray_graph). Intros gptr. assert (memory_block sh (sizeof t_wedgearray_graph) gptr = data_at_ sh (t_wedgearray_graph) gptr). { rewrite <- memory_block_data_at_; auto. } rewrite H0. clear H0. assert (data_at_ sh t_wedgearray_graph gptr = data_at sh t_wedgearray_graph (Vundef,(Vundef,Vundef)) gptr). { unfold data_at_, field_at_, data_at. assert (default_val (nested_field_type t_wedgearray_graph []) = (Vundef,(Vundef,Vundef))) by reflexivity. rewrite H0. auto. } rewrite H0. clear H0. assert_PROP (isptr gptr). entailer!. rename H0 into Hgptr. destruct gptr; inversion Hgptr. set (gptr:=ValidPointer b i). forward. forward_call (gv, sh, MAX_EDGES*(sizeof t_struct_edge)). Intros eptr. assert (memory_block sh (MAX_EDGES * (sizeof t_struct_edge)) eptr = data_at_ sh (tarray t_struct_edge MAX_EDGES) eptr). { assert (memory_block sh (MAX_EDGES*(sizeof t_struct_edge)) eptr = memory_block sh (sizeof (tarray t_struct_edge MAX_EDGES)) eptr). { simpl. auto. } rewrite <- memory_block_data_at_; auto. } rewrite H1. clear H1. assert (data_at_ sh (tarray t_struct_edge MAX_EDGES) eptr = data_at sh (tarray t_struct_edge MAX_EDGES) (Vundef_cwedges MAX_EDGES) eptr). { unfold data_at_, field_at_, data_at. assert (default_val (nested_field_type (tarray t_struct_edge MAX_EDGES) []) = repeat (Vundef, (Vundef, Vundef)) (Z.to_nat MAX_EDGES)) by reflexivity. rewrite H1. auto. } rewrite H1. clear H1. assert_PROP (isptr eptr). entailer!. rename H0 into Heptr. destruct eptr; inversion Heptr. set (eptr:=ValidPointer b0 i0). forward. forward. forward. forward. forward. Exists gptr eptr. entailer!. Qed.
imports: VST.floyd.proofauto VST.floyd.library CertiGraph.floyd_ext.share CertiGraph.lib.List_ext CertiGraph.graph.graph_model CertiGraph.graph.graph_gen CertiGraph.graph.path_lemmas CertiGraph.graph.graph_relation CertiGraph.msl_application.ArrayGraph CertiGraph.unionfind.env_unionfind_arr CertiGraph.kruskal.WeightedEdgeListGraph CertiGraph.kruskal.spatial_wedgearray_graph CertiGraph.kruskal.kruskal_specs CertiGraph.graph.undirected_uf_lemmas