support while loop with continue but no break, fixes #421

source/rust_verify_test/tests/loops.rs

@@ -1452,3 +1452,65 @@ test_verify_one_file! {
         }
     } => Ok(())
 }
+
+test_verify_one_file! {
+    #[test] loop_continue_no_break verus_code! {
+        fn test() {
+            let mut i = 0;
+            while i < 5
+                invariant i <= 5
+            {
+                continue;
+            }
+            assert(i == 5);
+        }
+
+        fn test_fail_beginning() {
+            let mut x = 0;
+            let mut i = 7;
+            while i < 5
+                invariant x == 1 // FAILS
+            {
+                x = 1;
+                continue;
+            }
+        }
+
+        fn test_fail_at_continue() {
+            let mut x = 2;
+            let mut i = 7;
+            while i < 5
+                invariant x == 2
+            {
+                x = 1;
+                continue; // FAILS
+            }
+        }
+
+        fn test_fail_at_end_after_continue(b: bool) {
+            let mut x = 2;
+            let mut i = 7;
+            while i < 5
+                invariant x == 2 // FAILS
+            {
+                if b {
+                    continue;
+                }
+                x = 1;
+            }
+        }
+
+        fn test_fail_at_end_after_continue_except_break(b: bool) {
+            let mut x = 2;
+            let mut i = 7;
+            loop
+                invariant_except_break x == 2 // FAILS
+            {
+                if b {
+                    continue;
+                }
+                x = 1;
+            }
+        }
+    } => Err(err) => assert_fails(err, 4)
+}

source/rust_verify_test/tests/loops_no_spinoff.rs

@@ -1362,3 +1362,56 @@ test_verify_one_file! {
         }
     } => Ok(())
 }
+
+test_verify_one_file! {
+    #[test] loop_continue_no_break_spinoff verus_code! {
+        fn test() {
+            let mut i = 0;
+            #[verifier::loop_isolation(false)]
+            while i < 5
+                invariant i <= 5
+            {
+                continue;
+            }
+            assert(i == 5);
+        }
+
+        fn test_fail_beginning() {
+            let mut x = 0;
+            let mut i = 0;
+            #[verifier::loop_isolation(false)]
+            while i < 5
+                invariant x == 1 // FAILS
+            {
+                x = 1;
+                continue;
+            }
+        }
+
+        fn test_fail_at_continue() {
+            let mut x = 2;
+            let mut i = 0;
+            #[verifier::loop_isolation(false)]
+            while i < 5
+                invariant x == 2
+            {
+                x = 1;
+                continue; // FAILS
+            }
+        }
+
+        fn test_fail_at_end_after_continue(b: bool) {
+            let mut x = 2;
+            let mut i = 0;
+            #[verifier::loop_isolation(false)]
+            while i < 5
+                invariant x == 2 // FAILS
+            {
+                if b {
+                    continue;
+                }
+                x = 1;
+            }
+        }
+    } => Err(err) => assert_fails(err, 3)
+}

source/vir/src/sst_to_air.rs

@@ -1967,7 +1967,7 @@ fn stm_to_stmts(ctx: &Ctx, state: &mut State, stm: &Stm) -> Result<Vec<Stmt>, Vi
             let is_air_break = *is_break && !loop_info.loop_isolation;
             let mut stmts: Vec<Stmt> = Vec::new();
             if !ctx.checking_spec_preconditions() && !is_air_break {
-                assert!(!loop_info.some_cond); // AST-to-SST conversion must eliminate the cond
+                assert!(!is_break || !loop_info.some_cond); // AST-to-SST conversion must eliminate the cond
                 if loop_info.is_for_loop && !*is_break {
                     // At the very least, the syntax macro will need to advance the ghost iterator
                     // at each continue.