From afb701040e23e2d308c1cb6d721c609f0ed8a119 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jon=C3=A1=C5=A1=20Fiala?= Date: Mon, 10 Jul 2023 13:04:15 +0200 Subject: [PATCH] Revert running Polonius on all bodies --- prusti/src/callbacks.rs | 13 +++++++------ 1 file changed, 7 insertions(+), 6 deletions(-) diff --git a/prusti/src/callbacks.rs b/prusti/src/callbacks.rs index 1610c382f31..9662e224818 100644 --- a/prusti/src/callbacks.rs +++ b/prusti/src/callbacks.rs @@ -2,7 +2,7 @@ use crate::verifier::verify; use prusti_common::config; use prusti_interface::{ environment::{mir_storage, Environment}, - specs::{self, cross_crate::CrossCrateSpecs}, + specs::{self, cross_crate::CrossCrateSpecs, is_spec_fn}, }; use prusti_rustc_interface::{ borrowck::consumers, @@ -32,11 +32,12 @@ fn mir_borrowck<'tcx>(tcx: TyCtxt<'tcx>, def_id: LocalDefId) -> &BorrowCheckResu // when calling `get_body_with_borrowck_facts`. TODO: figure out if we need // (anon) const bodies at all, and if so, how to get them? if !is_anon_const { - let body_with_facts = consumers::get_body_with_borrowck_facts( - tcx, - def_id, - consumers::ConsumerOptions::PoloniusOutputFacts, - ); + let consumer_opts = if is_spec_fn(tcx, def_id.to_def_id()) || config::no_verify() { + consumers::ConsumerOptions::RegionInferenceContext + } else { + consumers::ConsumerOptions::PoloniusOutputFacts + }; + let body_with_facts = consumers::get_body_with_borrowck_facts(tcx, def_id, consumer_opts); // SAFETY: This is safe because we are feeding in the same `tcx` that is // going to be used as a witness when pulling out the data. unsafe {