fact: Definition frame_shell_rep (sh: share) (fr: frame) (next: val) : mpred := match fr with {| fr_adr := a; fr_root := r; fr_roots := s |} => !! (field_compatible0 (tarray int_or_ptr_type (Zlength s)) nil r /\ WORD_SIZE * Zlength s <= Ptrofs.max_signed) && data_at sh (Tstruct _stack_frame noattr) (field_address0 (tarray int_or_ptr_type (Zlength s)) [ArraySubsc (Zlength s)] r, (r, next)) a end.
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