fact: Definition before_gc_thread_info_rep (sh: share) (ti: thread_info) (t: val) := let nursery := heap_head ti.(ti_heap) in let p := nursery.(space_start) in let n_lim := offset_val (WORD_SIZE * nursery.(total_space)) p in data_at sh thread_info_type (offset_val (WORD_SIZE * nursery.(used_space)) p, (n_lim, (ti.(ti_heap_p), (ti.(ti_args), (ti_fp ti, (Vptrofs (ti.(ti_nalloc)),nullval)))))) t * frames_rep sh (ti_frames ti) * heap_struct_rep sh ((p, (Vundef, (n_lim,n_lim))) :: map space_tri (tl ti.(ti_heap).(spaces))) ti.(ti_heap_p) * heap_rest_rep ti.(ti_heap).
imports: VST.veric.compcert_rmaps VST.msl.shares VST.msl.wand_frame VST.concurrency.conclib CertiGraph.lib.List_ext CertiGraph.msl_ext.log_normalize CertiGraph.msl_ext.ramification_lemmas CertiGraph.graph.graph_model CertiGraph.CertiGC.GCGraph CertiGraph.CertiGC.env_graph_gc CertiGraph.msl_ext.iter_sepcon Coq.Lists.List