fact: Record SingleFrame: Type := { local_assert: environ -> mpred; global_assert: environ -> mpred; stats: statement; real_frame: SingleFrame' local_assert global_assert stats }.
imports: CertiGraph.lib.Ensembles_ext CertiGraph.lib.Relation_ext CertiGraph.lib.List_ext CertiGraph.veric_ext.SeparationLogic CertiGraph.floyd_ext.ramification VST.floyd.base VST.floyd.canon VST.floyd.assert_lemmas VST.floyd.client_lemmas VST.floyd.closed_lemmas