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. - sep_apply (tree_in_graph_nonnull _ _ _ H0 H). Intros pl pr n tl tr. subst. Fail forward. assert_PROP (is_pointer_or_null pl). { entailer!. eauto. } assert_PROP (is_pointer_or_null pr). { entailer!. eauto. } localize [data_at Ews t_struct_tree (Vint n, (pl, pr)) p]. forward. unlocalize [graph_rep g]. { rewrite <- graph_rep_In; auto. } forward_call (g, tl, pl). localize [data_at Ews t_struct_tree (Vint n, (pl, pr)) p]. forward. unlocalize [graph_rep g]. { rewrite <- graph_rep_In; auto. } forward_call (g, tr, pr). localize [data_at Ews t_struct_tree (Vint n, (pl, pr)) p]. 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