Fixes after merge

viperproject · Oct 22, 2023 · f69cb0b · f69cb0b
1 parent 9f3b962
commit f69cb0b
Show file tree

Hide file tree

Showing 2 changed files with 17 additions and 0 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};

diff --git a/viper/src/verifier.rs b/viper/src/verifier.rs
@@ -70,6 +70,22 @@ impl<'a> Verifier<'a> {
         }
     }
 
+    #[tracing::instrument(level = "debug", skip_all)]
+    fn instantiate_verifier(
+        backend: VerificationBackend,
+        env: &'a JNIEnv,
+        reporter: JObject,
+        debug_info: JObject,
+    ) -> Result<JObject<'a>> {
+        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),
+        }
+    }
+
     #[must_use]
     #[tracing::instrument(level = "debug", skip_all)]
     pub fn initialize(self, args: &[String]) -> Self {