Use MIR without regions for pure functions.

viperproject · Jul 18, 2023 · db00af1 · db00af1
1 parent 95c4305
commit db00af1
Show file tree

Hide file tree

Showing 2 changed files with 10 additions and 12 deletions.
diff --git a/prusti-interface/src/environment/body.rs b/prusti-interface/src/environment/body.rs
@@ -321,15 +321,15 @@ impl<'tcx> EnvBody<'tcx> {
 
     pub(crate) fn load_pure_fn_body(&mut self, def_id: LocalDefId) {
         assert!(!self.pure_fns.local.contains_key(&def_id));
-        if config::no_verify() {
-            let body = Self::load_local_mir(self.tcx, def_id);
-            self.pure_fns.local.insert(def_id, body);
-        } else {
-            let bwbf = Self::load_local_mir_with_facts(self.tcx, def_id);
-            self.pure_fns.local.insert(def_id, bwbf.body.clone());
-            // Also add to `impure_fns` since we'll also be encoding this as impure
-            self.local_impure_fns.borrow_mut().insert(def_id, bwbf);
-        }
+        // if config::no_verify() {
+        let body = Self::load_local_mir(self.tcx, def_id);
+        self.pure_fns.local.insert(def_id, body);
+        // } else {
+        let bwbf = Self::load_local_mir_with_facts(self.tcx, def_id);
+        // self.pure_fns.local.insert(def_id, bwbf.body.clone());
+        // Also add to `impure_fns` since we'll also be encoding this as impure
+        self.local_impure_fns.borrow_mut().insert(def_id, bwbf);
+        // }
     }
 
     pub(crate) fn load_closure_body(&mut self, def_id: LocalDefId) {

diff --git a/prusti-viper/src/encoder/procedure_encoder.rs b/prusti-viper/src/encoder/procedure_encoder.rs
@@ -5511,10 +5511,8 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
             }
         } else {
             // FIXME: why are we getting the MIR body for this?
-            let mir = self.encoder.env().body.get_impure_fn_body(
+            let mir = self.encoder.env().body.get_impure_fn_body_identity(
                 containing_def_id.expect_local(),
-                // TODO(tymap): identity substs here are probably wrong?
-                self.encoder.env().query.identity_substs(containing_def_id),
             );
             let return_ty = mir.return_ty();
             let arg_tys = mir.args_iter().map(|arg| mir.local_decls[arg].ty).collect();