Rename verify_viper back to verify to comply with test suites

Author: JakuJ

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.

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{}",

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");
     }
 

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;
 }