From 6f666648874e6a3eb185eafc7b3e48140022c67f Mon Sep 17 00:00:00 2001
From: Jakub Janaszkiewicz <janaszkiewicz.jakub@gmail.com>
Date: Mon, 20 Mar 2023 22:38:48 +0100
Subject: [PATCH] Fixes after merge

---
 .../src/encoder/errors/error_manager.rs       | 20 ++++++++++++++++---
 viper/src/verifier.rs                         | 12 ++---------
 2 files changed, 19 insertions(+), 13 deletions(-)

diff --git a/prusti-viper/src/encoder/errors/error_manager.rs b/prusti-viper/src/encoder/errors/error_manager.rs
index 3bc9bd25b36..c79c28c9b28 100644
--- a/prusti-viper/src/encoder/errors/error_manager.rs
+++ b/prusti-viper/src/encoder/errors/error_manager.rs
@@ -6,6 +6,7 @@
 
 use super::PositionManager;
 use backend_common::VerificationError;
+use core::fmt::Debug;
 use log::debug;
 use prusti_interface::{data::ProcedureDefId, PrustiError};
 use prusti_rustc_interface::{errors::MultiSpan, span::source_map::SourceMap};
@@ -206,7 +207,11 @@ impl<'tcx> ErrorManager<'tcx> {
     }
 
     /// Register a new VIR position.
-    pub fn register_span<T: Into<MultiSpan> + Debug>(&mut self, def_id: ProcedureDefId, span: T) -> Position {
+    pub fn register_span<T: Into<MultiSpan> + Debug>(
+        &mut self,
+        def_id: ProcedureDefId,
+        span: T,
+    ) -> Position {
         self.position_manager.register_span(def_id, span)
     }
 
@@ -218,7 +223,11 @@ impl<'tcx> ErrorManager<'tcx> {
     /// Register the ErrorCtxt on an existing VIR position.
     #[tracing::instrument(level = "trace", skip(self))]
     pub fn set_error(&mut self, pos: Position, error_ctxt: ErrorCtxt) {
-        assert_ne!(pos, Position::default(), "Trying to register an error on a default position");
+        assert_ne!(
+            pos,
+            Position::default(),
+            "Trying to register an error on a default position"
+        );
         if let Some(existing_error_ctxt) = self.error_contexts.get(&pos.id()) {
             debug_assert_eq!(
                 existing_error_ctxt,
@@ -251,7 +260,12 @@ impl<'tcx> ErrorManager<'tcx> {
 
     /// Register a new VIR position with the given ErrorCtxt.
     /// Equivalent to calling `set_error` on the output of `register_span`.
-    pub fn register_error<T: Into<MultiSpan> + Debug>(&mut self, span: T, error_ctxt: ErrorCtxt, def_id: ProcedureDefId) -> Position {
+    pub fn register_error<T: Into<MultiSpan> + Debug>(
+        &mut self,
+        span: T,
+        error_ctxt: ErrorCtxt,
+        def_id: ProcedureDefId,
+    ) -> Position {
         let pos = self.register_span(def_id, span);
         self.set_error(pos, error_ctxt);
         pos
diff --git a/viper/src/verifier.rs b/viper/src/verifier.rs
index 7da53edea74..17f5e6cab8c 100644
--- a/viper/src/verifier.rs
+++ b/viper/src/verifier.rs
@@ -45,16 +45,7 @@ impl<'a> Verifier<'a> {
             };
 
             let debug_info = jni.new_seq(&[]);
-            match backend {
-                VerificationBackend::Silicon => {
-                    silicon::Silicon::with(env).new(reporter, debug_info)
-                }
-                VerificationBackend::Carbon => {
-                    carbon::CarbonVerifier::with(env).new(reporter, debug_info)
-                }
-                other => unreachable!("{:?} is not a Viper backend", other),
-            }
-            // TODO: WHAT IS Self::instantiate_verifier(backend, env, reporter, debug_info)
+            Self::instantiate_verifier(backend, env, reporter, debug_info)
         }));
 
         ast_utils.with_local_frame(16, || {
@@ -88,6 +79,7 @@ impl<'a> Verifier<'a> {
             VerificationBackend::Carbon => {
                 carbon::CarbonVerifier::with(env).new(reporter, debug_info)
             }
+            other => unreachable!("{:?} is not a Viper backend", other),
         }
     }