fact: Definition sum_spec := DECLARE _sum WITH t: tree, p: val PRE [ tptr t_struct_tree ] PROP() PARAMS (p) SEP (tree_rep t p) POST [ tuint ] PROP() LOCAL(temp ret_temp (Vint (sum t))) SEP (tree_rep t p).
imports: VST.floyd.proofauto VST.msl.iter_sepcon Demo.treeread