fact: Definition Gprog: funspecs := ltac:(with_library prog [test_int_or_ptr_spec; int_or_ptr_to_int_spec; int_or_ptr_to_ptr_spec; int_to_int_or_ptr_spec; ptr_to_int_or_ptr_spec; is_ptr_spec; Is_from_spec; abort_with_spec; forward_spec; forward_roots_spec; forward_remset_spec; do_scan_spec; do_generation_spec; create_space_spec; create_heap_spec; make_tinfo_spec; resume_spec; garbage_collect_spec]).
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