Fixes after rebase

viperproject · Oct 22, 2023 · 9aed8af · 9aed8af
1 parent 18bc02f
commit 9aed8af
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 17 deletions.
diff --git a/prusti-viper/src/encoder/procedure_encoder.rs b/prusti-viper/src/encoder/procedure_encoder.rs
@@ -76,7 +76,11 @@ use prusti_rustc_interface::{
     target::abi::{FieldIdx, Integer},
 };
 use rustc_hash::{FxHashMap, FxHashSet};
-use std::{collections::BTreeMap, convert::TryInto, fmt::Debug};
+use std::{
+    collections::BTreeMap,
+    convert::TryInto,
+    fmt::{Debug, Write},
+};
 use vir_crate::polymorphic::{
     self as vir, borrows::Borrow, collect_assigned_vars, compute_identifier, CfgBlockIndex,
     ExprIterator, Float, Successor, Type,

diff --git a/viper/src/verifier.rs b/viper/src/verifier.rs
@@ -73,22 +73,6 @@ 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 {