From 56b12e45410716c66f6d6e6dc70af346fe72ab5f Mon Sep 17 00:00:00 2001
From: Jakub Janaszkiewicz <janaszkiewicz.jakub@gmail.com>
Date: Tue, 28 Feb 2023 00:48:25 +0100
Subject: [PATCH] Add tests for loops, remove empty Conditional statements

---
 native-verifier/src/fol.rs                    |  9 ++++++
 native-verifier/src/smt_lib.rs                |  8 ++---
 prusti-server/src/backend.rs                  |  3 +-
 .../tests/verify/fail/native/while.rs         | 29 +++++++++++++++++++
 .../tests/verify/pass/native/while.rs         | 20 +++++++++++++
 5 files changed, 63 insertions(+), 6 deletions(-)
 create mode 100644 prusti-tests/tests/verify/fail/native/while.rs
 create mode 100644 prusti-tests/tests/verify/pass/native/while.rs

diff --git a/native-verifier/src/fol.rs b/native-verifier/src/fol.rs
index 153e514fb52..302858d544d 100644
--- a/native-verifier/src/fol.rs
+++ b/native-verifier/src/fol.rs
@@ -32,6 +32,15 @@ fn vir_statement_to_fol_statements(
 
             vec![FolStatement::Assume(eq)]
         }
+        Statement::Conditional(cond) => {
+            if !(cond.then_branch.is_empty() && cond.else_branch.is_empty()) {
+                log::warn!(
+                    "Conditional statement with non-empty branches, guard: {:?}",
+                    cond.guard
+                );
+            }
+            vec![]
+        }
         Statement::MethodCall(method_call) => {
             let method_decl = known_methods
                 .get(&method_call.method_name)
diff --git a/native-verifier/src/smt_lib.rs b/native-verifier/src/smt_lib.rs
index 15bc7099c31..c1731588ff5 100644
--- a/native-verifier/src/smt_lib.rs
+++ b/native-verifier/src/smt_lib.rs
@@ -357,6 +357,8 @@ impl SMTTranslatable for MethodDecl {
         // we assume these to be correct by default and collect their signatures
         if self.body.is_none() {
             smt.methods.insert(self.name.clone(), self.clone());
+        } else {
+            unimplemented!("Method bodies are not yet supported");
         }
     }
 }
@@ -430,11 +432,7 @@ impl SMTTranslatable for Expression {
                 ConstantValue::Int(i64) => i64.to_string(),
                 ConstantValue::BigInt(s) => s.clone(),
             },
-            Expression::MagicWand(magic_wand) => format!(
-                "(=> {} {})", // TODO: is this correct?
-                magic_wand.left.to_smt(),
-                magic_wand.right.to_smt()
-            ),
+            Expression::MagicWand(magic_wand) => unimplemented!("Magic wands"),
             Expression::PredicateAccessPredicate(_access) => {
                 // TODO: access predicates for predicates
                 warn!("PredicateAccessPredicate not supported");
diff --git a/prusti-server/src/backend.rs b/prusti-server/src/backend.rs
index 8bb63a744d1..9765bd3567e 100644
--- a/prusti-server/src/backend.rs
+++ b/prusti-server/src/backend.rs
@@ -1,4 +1,5 @@
 use crate::dump_viper_program;
+use backend_common::VerificationResult;
 use prusti_common::{
     config,
     vir::{LoweringContext, ToViper},
@@ -38,7 +39,7 @@ impl<'a> Backend<'a> {
                 })
             }
             Backend::Lithium(lithium) => {
-                Stopwatch::start("prusti-server", "verifierication");
+                Stopwatch::start("prusti-server", "vir verification");
                 lithium.verify(program)
             }
         }
diff --git a/prusti-tests/tests/verify/fail/native/while.rs b/prusti-tests/tests/verify/fail/native/while.rs
new file mode 100644
index 00000000000..710e2d521d6
--- /dev/null
+++ b/prusti-tests/tests/verify/fail/native/while.rs
@@ -0,0 +1,29 @@
+// compile-flags: -Pviper_backend=Lithium
+
+use prusti_contracts::*;
+
+const N: i32 = 10;
+
+#[requires(i <= N)]
+#[ensures(result == N)]
+fn wrong_invariant(i: i32) -> i32 {
+    let mut ret = i;
+    while ret < N {
+        body_invariant!(ret == i); //~ ERROR loop invariant might not hold
+        ret += 1;
+    }
+    ret
+}
+
+#[requires(i <= N)]
+#[ensures(result == N)] //~ ERROR might not hold
+fn weak_invariant(i: i32) -> i32 {
+    let mut ret = i;
+    while ret < N {
+        body_invariant!(ret <= N);
+        ret += 1;
+    }
+    ret
+}
+
+fn main() {}
diff --git a/prusti-tests/tests/verify/pass/native/while.rs b/prusti-tests/tests/verify/pass/native/while.rs
new file mode 100644
index 00000000000..90d1de2f199
--- /dev/null
+++ b/prusti-tests/tests/verify/pass/native/while.rs
@@ -0,0 +1,20 @@
+// compile-flags: -Pviper_backend=Lithium
+
+use prusti_contracts::*;
+
+const N: i32 = 10;
+
+#[requires(i <= N)]
+#[ensures(result == N)]
+fn test(i: i32) -> i32 {
+    let mut ret = i;
+    while ret < N {
+        body_invariant!(ret < N);
+        ret += 1;
+    }
+    ret
+}
+
+fn main() {
+    assert!(test(3) == N);
+}