add expected test

Author: thanhnguyen-aws

tests/expected/loop-contract/while_let_loop_for_slice.expected

@@ -0,0 +1,9 @@
+trim_ascii_start.loop_invariant_base.1\
+	 - Status: SUCCESS\
+	 - Description: "Check invariant before entry for loop trim_ascii_start.0"
+
+trim_ascii_start.loop_invariant_step.1\
+	 - Status: SUCCESS\
+	 - Description: "Check invariant after step for loop trim_ascii_start.0"
+
+VERIFICATION:- SUCCESSFUL

tests/expected/loop-contract/while_let_loop_for_slice.rs

@@ -0,0 +1,27 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// kani-flags: -Z loop-contracts
+
+//! Check if while-let invariant is correctly applied.
+
+#![feature(proc_macro_hygiene)]
+#![feature(stmt_expr_attributes)]
+
+#[kani::proof]
+fn trim_ascii_start() {
+    let mut a: [u8; 10] = kani::any();
+    let s = a.as_slice();
+    let mut bytes = s;
+    #[kani::loop_invariant(
+            bytes.len() <= s.len() &&
+            (bytes.len() == 0 || (&s[s.len()-bytes.len()..]).as_ptr() == bytes.as_ptr())
+    )]
+    while let [first, rest @ ..] = bytes {
+        if first.is_ascii_whitespace() {
+            bytes = rest;
+        } else {
+            break;
+        }
+    }
+}