fact: Definition append_spec := DECLARE _append WITH sh : share, x: val, y: val, s1: list val, s2: list val PRE [ tptr t_struct_list, tptr t_struct_list] PROP(writable_share sh) PARAMS (x;y) GLOBALS() SEP (lseg LS sh s1 x nullval; lseg LS sh s2 y nullval) POST [ tptr t_struct_list ] EX r: val, PROP() RETURN (r) SEP (lseg LS sh (s1++s2) r nullval).
imports: VST.floyd.proofauto CertiGraph.append.list_dt CertiGraph.append.append