tests: add tests for deterministic playback of the remaining primitive types (#1488)

* feat: add bool test

* feat: add nonzerou8 test

* feat: add array test

* feat: add result test

* feat: add option test

* feat: add custom test

* refactor: rename non_zero_u8 to non_zero

* chore: add newlines to all test files

* docs: make test case notes docstrings

Author: sanjit-bhat

tests/ui/exe-trace/array/expected

@@ -0,0 +1,15 @@
+VERIFICATION:- FAILED
+
+Executable trace
+```
+#[test]
+fn kani_exe_trace_harness
+    let det_vals: Vec<Vec<u8>> = vec![
+        // 101
+        vec![101],
+        // 102
+        vec![102]
+    ];
+    kani::exe_trace_run(det_vals, harness);
+}
+```

tests/ui/exe-trace/array/main.rs

@@ -0,0 +1,11 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// kani-flags: --harness harness --enable-unstable --gen-exe-trace
+
+#[kani::proof]
+#[kani::unwind(10)]
+pub fn harness() {
+    let arr_1: [u8; 2] = kani::any();
+    assert!(!(arr_1[0] == 101 && arr_1[1] == 102));
+}

tests/ui/exe-trace/bool/expected

@@ -0,0 +1,13 @@
+VERIFICATION:- FAILED
+
+Executable trace
+```
+#[test]
+fn kani_exe_trace_harness
+    let det_vals: Vec<Vec<u8>> = vec![
+        // 0
+        vec![0
+    ];
+    kani::exe_trace_run(det_vals, harness);
+}
+```

tests/ui/exe-trace/bool/main.rs

@@ -0,0 +1,11 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// kani-flags: --harness harness --enable-unstable --gen-exe-trace
+
+/// Note: We can't test a false value yet because any::<bool>() could be any non-zero number.
+#[kani::proof]
+pub fn harness() {
+    let bool_1: bool = kani::any();
+    assert!(bool_1 != true);
+}

tests/ui/exe-trace/custom/expected

@@ -0,0 +1,15 @@
+VERIFICATION:- FAILED
+
+Executable trace
+```
+#[test]
+fn kani_exe_trace_harness
+    let det_vals: Vec<Vec<u8>> = vec![
+        // 101
+        vec![101],
+        // 102
+        vec![102, 0]
+    ];
+    kani::exe_trace_run(det_vals, harness);
+}
+```

tests/ui/exe-trace/custom/main.rs

@@ -0,0 +1,21 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// kani-flags: --harness harness --enable-unstable --gen-exe-trace
+
+struct MyStruct {
+    field1: u8,
+    field2: u16,
+}
+
+impl kani::Arbitrary for MyStruct {
+    fn any() -> Self {
+        MyStruct { field1: kani::any(), field2: kani::any() }
+    }
+}
+
+#[kani::proof]
+pub fn harness() {
+    let my_struct: MyStruct = kani::any();
+    assert!(!(my_struct.field1 == 101 && my_struct.field2 == 102));
+}

tests/ui/exe-trace/f32/expected

@@ -24,4 +24,4 @@ fn kani_exe_trace_harness
     ];
     kani::exe_trace_run(det_vals, harness);
 }
-```
+```

tests/ui/exe-trace/f32/main.rs

@@ -3,6 +3,7 @@
 
 // kani-flags: --harness harness --enable-unstable --gen-exe-trace
 
+/// Note: Don't include NaN because there are multiple possible NaN values.
 #[kani::proof]
 pub fn harness() {
     let f32_1: f32 = kani::any();
@@ -23,5 +24,4 @@ pub fn harness() {
             && f32_7 == f32::MAX
             && f32_8 == f32::INFINITY)
     );
-    // Note: Don't include NaN because there are multiple possible NaN values.
 }

tests/ui/exe-trace/f64/expected

@@ -24,4 +24,4 @@ fn kani_exe_trace_harness
     ];
     kani::exe_trace_run(det_vals, harness);
 }
-```
+```

tests/ui/exe-trace/f64/main.rs

@@ -3,6 +3,7 @@
 
 // kani-flags: --harness harness --enable-unstable --gen-exe-trace
 
+/// Note: Don't include NaN because there are multiple possible NaN values.
 #[kani::proof]
 pub fn harness() {
     let f64_1: f64 = kani::any();
@@ -23,5 +24,4 @@ pub fn harness() {
             && f64_7 == f64::MAX
             && f64_8 == f64::INFINITY)
     );
-    // Note: Don't include NaN because there are multiple possible NaN values.
 }