Struct GhostStatements 

pub(crate) struct GhostStatements {
    at_start: Vec<GhostStatement>,
    at_location: UnordMap<Location, Vec<GhostStatement>>,
    at_edge: UnordMap<BasicBlock, FxHashMap<BasicBlock, Vec<GhostStatement>>>,
}

Fields

at_start: Vec<GhostStatement>

at_location: UnordMap<Location, Vec<GhostStatement>>

at_edge: UnordMap<BasicBlock, FxHashMap<BasicBlock, Vec<GhostStatement>>>

Implementations

impl GhostStatements

fn new(genv: GlobalEnv<'_, '_>, checker_id: CheckerId) -> QueryResult<Self>

fn add_unblocks<'tcx>(&mut self, tcx: TyCtxt<'tcx>, body_root: &BodyRoot<'tcx>)

fn insert_at(&mut self, point: Point, stmt: GhostStatement)

fn extend_at( &mut self, point: Point, stmts: impl IntoIterator<Item = GhostStatement>, )

fn at(&mut self, point: Point) -> StatementsAt<'_>

pub(crate) fn statements_at( &self, point: Point, ) -> impl Iterator<Item = &GhostStatement>

pub(crate) fn dump_ghost_mir<'tcx>(&self, tcx: TyCtxt<'tcx>, body: &Body<'tcx>)