rapx/verify/property_checker/
alias.rs

1#[cfg(not(rapx_has_skip_norm_wip))]
2use crate::compat::SkipNormWip;
3use z3::Solver;
4use crate::verify::contract::Property;
5use crate::verify::report::CheckResult;
6use crate::helpers::mir_scan::Checkpoint;
7use crate::verify::vm::state::VmState;
8
9use super::PropertyChecker;
10
11impl PropertyChecker {
12    pub(super) fn check_alias<'ctx, 'tcx>(&self, vm_state: &VmState<'ctx, 'tcx>, _solver: &Solver<'ctx>,
13        checkpoint: &Checkpoint<'tcx>, property: &Property<'tcx>) -> CheckResult
14    {
15        match crate::verify::vm::alias::check_alias_vm(vm_state, checkpoint, property) {
16            crate::verify::vm::alias::VmAliasResult::Proved => CheckResult::Proved,
17            crate::verify::vm::alias::VmAliasResult::Failed(_msg) => CheckResult::Failed,
18            crate::verify::vm::alias::VmAliasResult::Unknown => CheckResult::Unknown,
19        }
20    }
21
22    pub(super) fn check_owning<'ctx, 'tcx>(&self, vm_state: &VmState<'ctx, 'tcx>, _solver: &Solver<'ctx>,
23        checkpoint: &Checkpoint<'tcx>, property: &Property<'tcx>) -> CheckResult
24    {
25        let Some(value) = self.target_value(vm_state, checkpoint, property) else { return CheckResult::Unknown };
26        if let Some(id) = value.provenance_alloc_id() {
27            if vm_state.alloc(id).dead { return CheckResult::Failed; }
28            return CheckResult::Proved;
29        }
30        CheckResult::Unknown
31    }
32}
rapx/verify/property_checker/alias.rs

rapx/verify/property_checker/
alias.rs
