wip

Author: Aurel300

prusti-interface/src/environment/body.rs

@@ -169,9 +169,13 @@ impl<'tcx> EnvBody<'tcx> {
             let monomorphised = if let Some(caller_def_id) = caller_def_id {
                 let param_env = self.tcx.param_env(caller_def_id);
                 self.tcx
-                    .subst_and_normalize_erasing_regions(substs, param_env, body.0)
+                    .subst_and_normalize_erasing_regions(
+                        substs,
+                        param_env,
+                        ty::EarlyBinder::bind(body.0),
+                    )
             } else {
-                ty::EarlyBinder(body.0).subst(self.tcx, substs)
+                ty::EarlyBinder::bind(body.0).subst(self.tcx, substs)
             };
             v.insert(MirBody(monomorphised)).clone()
         } else {

prusti-interface/src/environment/diagnostic.rs

@@ -44,7 +44,7 @@ impl<'tcx> EnvDiagnostic<'tcx> {
         help: &Option<String>,
         notes: &[(String, Option<S>)],
     ) {
-        let mut diagnostic = self.tcx.sess.struct_err(msg);
+        let mut diagnostic = self.tcx.sess.struct_err(msg.to_string());
         Self::configure_diagnostic(&mut diagnostic, sp, help, notes);
         for warn in self.warn_buffer.borrow_mut().iter_mut() {
             self.tcx.sess.diagnostic().emit_diagnostic(warn);
@@ -60,7 +60,7 @@ impl<'tcx> EnvDiagnostic<'tcx> {
         help: &Option<String>,
         notes: &[(String, Option<S>)],
     ) {
-        let mut diagnostic = self.tcx.sess.struct_warn(msg);
+        let mut diagnostic = self.tcx.sess.struct_warn(msg.to_string());
         Self::configure_diagnostic(&mut diagnostic, sp, help, notes);
         diagnostic.emit();
     }
@@ -73,7 +73,7 @@ impl<'tcx> EnvDiagnostic<'tcx> {
         help: &Option<String>,
         notes: &[(String, Option<S>)],
     ) {
-        let mut diagnostic = self.tcx.sess.struct_warn(msg);
+        let mut diagnostic = self.tcx.sess.struct_warn(msg.to_string());
         Self::configure_diagnostic(&mut diagnostic, sp, help, notes);
         diagnostic.buffer(&mut self.warn_buffer.borrow_mut());
     }

prusti-interface/src/environment/query.rs

@@ -161,7 +161,7 @@ impl<'tcx> EnvQuery<'tcx> {
     ) -> ty::PolyFnSig<'tcx> {
         let def_id = def_id.into_param();
         let sig = if self.tcx.is_closure(def_id) {
-            ty::EarlyBinder(substs.as_closure().sig())
+            ty::EarlyBinder::bind(substs.as_closure().sig())
         } else {
             self.tcx.fn_sig(def_id)
         };
@@ -255,7 +255,7 @@ impl<'tcx> EnvQuery<'tcx> {
         // more precisely. We can do this directly with `impl_method_substs`
         // because they contain the substs for the `impl` block as a prefix.
         let call_trait_substs =
-            ty::EarlyBinder(trait_ref.substs).subst(self.tcx, impl_method_substs);
+            ty::EarlyBinder::bind(trait_ref.substs).subst(self.tcx, impl_method_substs);
         let impl_substs = self.identity_substs(impl_def_id);
         let trait_method_substs = self.tcx.mk_substs_from_iter(
             call_trait_substs
@@ -284,7 +284,7 @@ impl<'tcx> EnvQuery<'tcx> {
             debug!("Fetching implementations of method '{:?}' defined in trait '{}' with substs '{:?}'", proc_def_id, self.tcx.def_path_str(trait_id), substs);
             let infcx = self.tcx.infer_ctxt().build();
             let mut sc = SelectionContext::new(&infcx);
-            let trait_ref = self.tcx.mk_trait_ref(trait_id, substs);
+            let trait_ref = ty::TraitRef::new(self.tcx, trait_id, substs);
             let obligation = Obligation::new(
                 self.tcx,
                 ObligationCause::dummy(),

prusti-viper/src/encoder/encoder.rs

@@ -308,7 +308,7 @@ impl<'v, 'tcx> Encoder<'v, 'tcx> {
         ct: mir::UnevaluatedConst<'tcx>,
     ) -> Option<mir::interpret::Scalar> {
         let tcx = self.env.tcx();
-        let param_env = tcx.param_env(ct.def.did);
+        let param_env = tcx.param_env(ct.def);
         tcx.const_eval_resolve(param_env, ct, None)
             .ok()
             .and_then(|const_value| const_value.try_to_scalar())

prusti-viper/src/encoder/mir/contracts/borrows.rs

@@ -44,7 +44,7 @@ impl<P: fmt::Debug> fmt::Display for BorrowInfo<P> {
     fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
         let lifetime = match self.region {
             None => "static".to_string(),
-            Some(ty::BoundRegionKind::BrAnon(id, _)) => format!("#{id}"),
+            Some(ty::BoundRegionKind::BrAnon(_)) => "anon".to_string(),
             Some(ty::BoundRegionKind::BrNamed(_, name)) => name.to_string(),
             _ => unimplemented!(),
         };

prusti-viper/src/encoder/mir/procedures/encoder/builtin_function_encoder.rs

@@ -12,7 +12,7 @@ pub(super) trait BuiltinFuncAppEncoder<'p, 'v, 'tcx> {
         args: &[mir::Operand<'tcx>],
         destination: mir::Place<'tcx>,
         target: &Option<mir::BasicBlock>,
-        cleanup: &Option<mir::BasicBlock>,
+        unwind: mir::UnwindAction,
     ) -> SpannedEncodingResult<bool>;
 }
 
@@ -28,7 +28,7 @@ impl<'p, 'v, 'tcx> BuiltinFuncAppEncoder<'p, 'v, 'tcx> for super::ProcedureEncod
         args: &[mir::Operand<'tcx>],
         destination: mir::Place<'tcx>,
         target: &Option<mir::BasicBlock>,
-        cleanup: &Option<mir::BasicBlock>,
+        unwind: mir::UnwindAction,
     ) -> SpannedEncodingResult<bool> {
         let full_called_function_name = self
             .encoder
@@ -192,9 +192,9 @@ impl<'p, 'v, 'tcx> BuiltinFuncAppEncoder<'p, 'v, 'tcx> for super::ProcedureEncod
                     debug!("Absence of panic will not be checked")
                 }
                 assert!(target.is_none());
-                if let Some(cleanup) = cleanup {
+                if let mir::UnwindAction::Cleanup(cleanup) = unwind {
                     let successor =
-                        vir_high::Successor::Goto(self.encode_basic_block_label(*cleanup));
+                        vir_high::Successor::Goto(self.encode_basic_block_label(cleanup));
                     block_builder.set_successor_jump(successor);
                 } else {
                     unimplemented!();