proposition: Lemma gather_thread_info_rep: forall (v1 v2: val) sh t_info ti , data_at sh thread_info_type (v1,(v2, (ti_heap_p t_info, (ti_args t_info,(ti_fp t_info, (Vptrofs(ti_nalloc t_info),nullval)))))) ti * frames_rep sh (ti_frames t_info) * data_at sh heap_type (@map space (val * (val * (val*val))) space_tri (spaces (ti_heap t_info))) (ti_heap_p t_info) * heap_rest_rep (ti_heap t_info) |-- thread_info_rep sh t_info ti.
proof: Proof. intros. unfold thread_info_rep, heap_rep, heap_struct_rep. do 2 unfold_data_at (data_at _ thread_info_type _ _). cancel. Qed.
imports: CertiGraph.CertiGC(env_graph_gc gc_spec)