fact: Definition garbage_collect_spec := DECLARE _garbage_collect WITH rsh: share, sh: share, gv: globals, ti: val, g: LGraph, t_info: thread_info, roots : roots_t, outlier: outlier_t PRE [tptr thread_info_type] PROP (readable_share rsh; writable_share sh; super_compatible g (ti_heap t_info) (frames2rootpairs (ti_frames t_info)) roots outlier; garbage_collect_condition g (ti_heap t_info); safe_to_copy g) PARAMS (ti) GLOBALS (gv) SEP (mem_mgr gv; all_string_constants rsh gv; outlier_rep outlier; graph_rep g; before_gc_thread_info_rep sh t_info ti; ti_token_rep (ti_heap t_info) (ti_heap_p t_info)) POST [tvoid] EX g': LGraph, EX t_info': thread_info, EX roots': roots_t, PROP (super_compatible g' (ti_heap t_info') (frames2rootpairs (ti_frames t_info')) roots' outlier; garbage_collect_relation roots roots' g g'; garbage_collect_condition g' (ti_heap t_info'); safe_to_copy g'; frame_shells_eq (ti_frames t_info) (ti_frames t_info'); Ptrofs.unsigned (ti_nalloc t_info) <= total_space (heap_head (ti_heap t_info')) - used_space (heap_head (ti_heap t_info'))) RETURN () SEP (mem_mgr gv; all_string_constants rsh gv; outlier_rep outlier; graph_rep g'; before_gc_thread_info_rep sh t_info' ti; ti_token_rep (ti_heap t_info') (ti_heap_p t_info')).
imports: VST.veric.rmaps CertiGraph.lib.List_ext CertiGraph.graph.graph_model CertiGraph.CertiGC.GCGraph CertiGraph.CertiGC.spatial_gcgraph CertiGraph.CertiGC.env_graph_gc CertiGraph.msl_ext.iter_sepcon