proposition: Lemma body_sum: semax_body Vprog Gprog f_sum sum_spec.
proof: Proof. start_function. forward_if. eauto with valid_pointer. - subst. sep_apply (tree_in_graph_null _ _ H). forward. - inversion H; subst. now exfalso. assert_PROP (is_pointer_or_null (dst g (p, L))). { entailer!. eauto. } assert_PROP (is_pointer_or_null (dst g (p, R))). { entailer!. eauto. } localize [vertex_at p (vgamma g p)]. simpl vertex_at. forward. unlocalize [graph_rep g]. { rewrite <- graph_rep_In; auto. } forward_call (g, tl, (dst g (p, L))). localize [vertex_at p (vgamma g p)]. simpl vertex_at. forward. unlocalize [graph_rep g]. { rewrite <- graph_rep_In; auto. } forward_call (g, tr, (dst g (p, R))). localize [vertex_at p (vgamma g p)]. simpl vertex_at. forward. unlocalize [graph_rep g]. { rewrite <- graph_rep_In; auto. } forward. entailer!. now rewrite Int.add_assoc. Qed.
imports: VST.floyd.proofauto VST.msl.iter_sepcon Demo.treeread CertiGraph.graph.graph_model CertiGraph.msl_application.Graph