Add tests for loops, remove empty Conditional statements

Author: JakuJ

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)

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

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

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() {}

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