Struct TypedContext 

struct TypedContext<'a, 'tcx> {
    checker: &'a SmtChecker<'tcx>,
    caller: DefId,
    forward: &'a ForwardVisitResult<'tcx>,
    required_ty: Ty<'tcx>,
}

Fields

checker: &'a SmtChecker<'tcx>

caller: DefId

forward: &'a ForwardVisitResult<'tcx>

required_ty: Ty<'tcx>

Implementations

impl<'a, 'tcx> TypedContext<'a, 'tcx>

fn place_is_typed( &mut self, place: &PlaceKey, seen: &mut HashSet<PlaceKey>, depth: usize, ) -> bool

Prove that a place denotes storage or a pointer whose dynamic type is required_ty.

fn value_is_typed( &mut self, value: &AbstractValue<'tcx>, seen: &mut HashSet<PlaceKey>, depth: usize, ) -> bool

Prove that an abstract value carries required_ty typed provenance.

fn latest_value_for_place( &self, place: &PlaceKey, ) -> Option<AbstractValue<'tcx>>

Return the latest value assigned to a place in the retained path slice.

fn latest_cast_source_for_place( &self, place: &PlaceKey, ) -> Option<AbstractValue<'tcx>>

Return the latest cast source retained for a target place.

fn latest_points_to_source(&self, place: &PlaceKey) -> Option<PlaceKey>

Return the latest provenance source retained for a pointer place.

fn known_init_matches(&self, place: &PlaceKey) -> bool

Return true when a previous write initialized this place as required_ty.

fn storage_place_is_typed(&self, place: &PlaceKey) -> bool

Return true when a Rust storage place itself is known to contain required_ty.

fn place_ty(&self, place: &PlaceKey) -> Option<Ty<'tcx>>

Resolve a place type from MIR locals and field projections.

fn ty_has_required_payload(&self, ty: Ty<'tcx>) -> bool

Return true when ty or its pointer/reference payload is required_ty.

fn ty_matches(&self, ty: Ty<'tcx>) -> bool

Return true when two compiler types are the same for current verifier purposes.

fn ty_name_matches(&self, ty_name: &str) -> bool

Return true when a stringly fact type name matches required_ty.