Fixes after merge

viperproject · Mar 20, 2023 · 6f66664 · 6f66664
1 parent e7de04e
commit 6f66664
Show file tree

Hide file tree

Showing 2 changed files with 19 additions and 13 deletions.
diff --git 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
@@ -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),
         }
     }