Struct ForEachFacts 

pub(crate) struct ForEachFacts<'z3, 'tcx> {
    pub target_ty: Option<Ty<'tcx>>,
    pub aligned_ty: Option<Ty<'tcx>>,
    pub allocated: Option<(Ty<'tcx>, Int<'z3>)>,
    pub owning: bool,
}

Uniform facts about the pointer elements of a container, established by x.iter() for_each invariants.

Each fact is a property every element pointer satisfies. The facts are anchored to the container’s allocation (not the container value) because a pointer loaded from the container resolves its provenance through this allocation, so the checker finds the fact via the loaded pointer’s provenance.

Fields

target_ty: Option<Ty<'tcx>>

Typed(iter(), T): every element pointer points at a valid T.

aligned_ty: Option<Ty<'tcx>>

Align(iter(), T): every element pointer is aligned to align_of(T).

allocated: Option<(Ty<'tcx>, Int<'z3>)>

Allocated(iter(), T, n): every element pointer backs >= n T elements (n may be symbolic).

owning: bool

Owning(iter()): every element pointer is the sole owner of its pointee (mutually non-aliasing). Established by the trusted invariant; the aliasing check of the invariant itself is done by the alias analysis, not by this flag.

Trait Implementations

impl<'z3, 'tcx> Clone for ForEachFacts<'z3, 'tcx>

fn clone(&self) -> Self

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl<'z3, 'tcx> Debug for ForEachFacts<'z3, 'tcx>

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl<'z3, 'tcx> Default for ForEachFacts<'z3, 'tcx>

fn default() -> Self

Returns the “default value” for a type.