From 23b7abdedee95c669d287309808f2401b13377bf Mon Sep 17 00:00:00 2001
From: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com>
Date: Fri, 15 Sep 2023 11:59:33 -0700
Subject: [PATCH] Add range demo example (#2772)

---
 .../demos/non-empty-range/Cargo.toml          | 11 +++++
 .../non-empty-range/check_range.expected      |  4 ++
 .../demos/non-empty-range/src/lib.rs          | 49 +++++++++++++++++++
 3 files changed, 64 insertions(+)
 create mode 100644 tests/cargo-kani/demos/non-empty-range/Cargo.toml
 create mode 100644 tests/cargo-kani/demos/non-empty-range/check_range.expected
 create mode 100644 tests/cargo-kani/demos/non-empty-range/src/lib.rs

diff --git a/tests/cargo-kani/demos/non-empty-range/Cargo.toml b/tests/cargo-kani/demos/non-empty-range/Cargo.toml
new file mode 100644
index 0000000000000..768167573e476
--- /dev/null
+++ b/tests/cargo-kani/demos/non-empty-range/Cargo.toml
@@ -0,0 +1,11 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+[package]
+name = "non-empty-range"
+version = "0.1.0"
+edition = "2021"
+description = "A demo example for Kani that shows how to go from partial assurance with unit tests to full assurance with Kani"
+
+# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
+
+[dependencies]
diff --git a/tests/cargo-kani/demos/non-empty-range/check_range.expected b/tests/cargo-kani/demos/non-empty-range/check_range.expected
new file mode 100644
index 0000000000000..c0c666fca1011
--- /dev/null
+++ b/tests/cargo-kani/demos/non-empty-range/check_range.expected
@@ -0,0 +1,4 @@
+Status: SUCCESS\
+Description: "assertion failed: range.is_none() || !range.as_ref().unwrap().is_empty()"
+
+VERIFICATION:- SUCCESSFUL
diff --git a/tests/cargo-kani/demos/non-empty-range/src/lib.rs b/tests/cargo-kani/demos/non-empty-range/src/lib.rs
new file mode 100644
index 0000000000000..9cb96a7c1bc3f
--- /dev/null
+++ b/tests/cargo-kani/demos/non-empty-range/src/lib.rs
@@ -0,0 +1,49 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+/// a helper function that given a pair of integers, returns a valid non-empty
+/// range (if possible) or `None`
+pub fn create_non_empty_range(a: i32, b: i32) -> Option<std::ops::Range<i32>> {
+    let range = if a < b {
+        Some(a..b)
+    } else if b < a {
+        Some(b..a)
+    } else {
+        None
+    };
+    assert!(range.is_none() || !range.as_ref().unwrap().is_empty());
+    range
+}
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+
+    #[test]
+    fn test_create_range1() {
+        let r = create_non_empty_range(5, 9);
+        assert_eq!(r.unwrap(), 5..9);
+    }
+
+    #[test]
+    fn test_create_range2() {
+        let r = create_non_empty_range(35, 2);
+        assert_eq!(r.unwrap(), 2..35);
+    }
+
+    #[test]
+    fn test_create_range3() {
+        let r = create_non_empty_range(-5, -5);
+        assert!(r.is_none());
+    }
+}
+
+#[cfg(kani)]
+mod kani_checks {
+    use super::*;
+
+    #[kani::proof]
+    fn check_range() {
+        create_non_empty_range(kani::any(), kani::any());
+    }
+}