Skip to main content

field_invariant_check

rapx::verify::property_checker::auto_trait

Function field_invariant_check 

Source 
pub(crate) fn field_invariant_check<'tcx>(
    tcx: TyCtxt<'tcx>,
    ty: Ty<'tcx>,
    kind: PropertyKind,
    field: Option<&str>,
    invariant_results: &FxHashMap<DefId, CheckResult>,
) -> CheckResult
Expand description

Type-level Allocated(ptr, T, n) / Owning(ptr) obligation check (no VM state required): Proved when T declares a matching #[rapx::invariant(Allocated(ptr))] / #[rapx::invariant(Owning(ptr))] annotation (optionally restricted to the field named in the property) and the already-run struct-invariant verification discharged it. invariant_results carries the per-struct verdict; when a struct’s invariants failed to verify, the check fails too.