Rename verify_viper back to verify to comply with test suites

viperproject · Feb 15, 2023 · ce3234e · ce3234e
1 parent 4066fb1
commit ce3234e
Show file tree

Hide file tree

Showing 4 changed files with 4 additions and 4 deletions.
diff --git a/prusti-server/src/process_verification.rs b/prusti-server/src/process_verification.rs
@@ -196,7 +196,7 @@ pub fn process_verification_request<'v, 't: 'v>(
                 panic!("Lithium backend can only verify vir::low programs");
             }
         } else {
-            verifier.verify_viper(viper_program)
+            verifier.verify(viper_program)
         };
 
         // Don't cache Java exceptions, which might be due to misconfigured paths.

diff --git a/viper/src/jvm_verifier.rs b/viper/src/jvm_verifier.rs
@@ -109,7 +109,7 @@ impl<'a> Verifier<'a> for JavaBasedVerifier<'a> {
         panic!("VIR verification is not supported by JVM-based verifiers.");
     }
 
-    fn verify_viper(&mut self, program: Program) -> VerificationResult {
+    fn verify(&mut self, program: Program) -> VerificationResult {
         self.ast_utils.with_local_frame(16, || {
             debug!(
                 "Program to be verified:\n{}",

diff --git a/viper/src/native_backend/native_verifier.rs b/viper/src/native_backend/native_verifier.rs
@@ -37,7 +37,7 @@ impl<'a> Verifier<'a> for NativeVerifier {
         // TODO: Start the verifier
     }
 
-    fn verify_viper(&mut self, _program: crate::Program) -> VerificationResult {
+    fn verify(&mut self, _program: crate::Program) -> VerificationResult {
         panic!("Viper verification not supported by Lithium");
     }
 

diff --git a/viper/src/verifier.rs b/viper/src/verifier.rs
@@ -11,7 +11,7 @@ pub trait Verifier<'a> {
 
     fn start(&mut self);
 
-    fn verify_viper(&mut self, program: crate::Program) -> VerificationResult;
+    fn verify(&mut self, program: crate::Program) -> VerificationResult;
 
     fn verify_vir(&mut self, program: &vir::low::Program) -> VerificationResult;
 }