fact: Definition forward_roots_spec := DECLARE _forward_roots WITH rsh: share, sh: share, gv: globals, g: LGraph, h: heap, hp: val, fr: list frame, roots: roots_t, outlier: outlier_t, from: nat, to: nat PRE [tptr int_or_ptr_type, tptr int_or_ptr_type, tptr (tptr int_or_ptr_type), tptr (Tstruct _stack_frame noattr)] PROP (readable_share rsh; writable_share sh; super_compatible g h (frames2rootpairs fr) roots outlier; forward_condition g h from to; from <> to) PARAMS (gen_start g from; limit_address g h from; heap_next_address hp to; frames_p fr) GLOBALS (gv) SEP (all_string_constants rsh gv; outlier_rep outlier; graph_rep g; frames_rep sh fr; heap_rep sh h hp) POST [tvoid] EX g' : LGraph, EX h': heap, EX roots': roots_t, PROP (super_compatible g' h' (frames2rootpairs (update_frames fr (map (root2val g') roots'))) roots' outlier; forward_roots_relation from to roots g roots' g'; forward_condition g' h' from to; heap_relation h h') RETURN () SEP (all_string_constants rsh gv; outlier_rep outlier; graph_rep g'; frames_rep sh (update_frames fr (map (root2val g') roots')); heap_rep sh h' hp).
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