Add Rust package with manual tests (#127)

resources/test-crates/simple-test/Cargo.toml

@@ -0,0 +1,11 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+[package]
+name = "simple-test"
+version = "0.1.0"
+edition = "2021"
+
+# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
+
+[dependencies]

resources/test-crates/simple-test/src/funs.rs

@@ -0,0 +1,35 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+pub fn estimate_size(x: u32) -> u32 {
+ assert!(x < 4096);
+
+ if x < 256 {
+ if x < 128 {
+ return 1;
+ } else {
+ return 3;
+ }
+ } else if x < 1024 {
+ if x > 1022 {
+ return 4;
+ } else {
+ return 5;
+ }
+ } else {
+ if x < 2048 {
+ return 7;
+ } else {
+ return 9;
+ }
+ }
+}
+
+pub fn find_index(nums: &[i32], target: i32) -> Option<usize> {
+ for (index, &num) in nums.iter().enumerate() { // coverage should be yellow
+ if num == target { // coverage should be green
+ return Some(index); // coverage should be green
+ }
+ }
+ None // coverage should be red
+} // coverage should be yellow

resources/test-crates/simple-test/src/lib.rs

@@ -0,0 +1,57 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! This package is intended to assist in manually testing the features of the
+//! extension. The tests to be performed are the following:
+//!
+//! 1. Run verification for `test_success` and check that it passes.
+//! 2. Run verification for `test_failure` and check that it fails with
+//! "assertion failed: x < 4096".
+//! 3. Click on "Generate concrete test for test_failure" and check that a new
+//! Rust unit test is added after "test_failure".
+//! 4. Check that the actions "Run Test (Kani)" and "Debug Harness (Kani)"
+//! appear above the Rust unit test that was generated in the previous step.
+//! 5. Click on the "Run Test (Kani)" action. Check that the test runs on a
+//! terminal and it panics as expected.
+//! 6. Click on the "Debug Harness (Kani)" action. Check that the debugging mode
+//! is started (debugging controls should appear on the top) and stop it by
+//! clicking on the red square button.
+//! 7. Toggle on the "Codelens-kani: Highlight" option in "Settings > Kani".
+//! 8. Check that the "Get coverage info" action appears for the "test_success"
+//! and "test_failure" harnesses.
+//! 9. Run the "Get coverage info" action for "test_coverage". Check that all
+//! lines in "test_coverage" are green. In addition, check that in
+//! "funs::find_index":
+//! - The first and last highlighted lines are yellow.
+//! - The second and third highlighted lines are green.
+//! - The remaining highlighted line is red.
+//! Comments indicating the correct colors are available in "funs::find_index".
+mod funs;
+
+#[cfg(kani)]
+mod verify {
+ use super::*;
+
+ #[kani::proof]
+ fn test_success() {
+ let x: u32 = kani::any();
+ kani::assume(x < 4096);
+ let y = funs::estimate_size(x);
+ assert!(y < 10);
+ }
+
+ #[kani::proof]
+ fn test_failure() {
+ let x: u32 = kani::any();
+ let y = funs::estimate_size(x);
+ assert!(y < 10);
+ }
+
+ #[kani::proof]
+ fn test_coverage() {
+ let numbers = [10, 20, 30, 40, 50];
+ let target = 30;
+ let result = funs::find_index(&numbers, target);
+ assert_eq!(result, Some(2));
+ }
+}