From b751ad8698404be4405f4a0d3c5cd22d83e8b733 Mon Sep 17 00:00:00 2001
From: Zyad Hassan <zyadh@amazon.com>
Date: Tue, 1 Oct 2024 14:34:25 -0700
Subject: [PATCH] Add back test

---
 tests/cargo-kani/mir-linker/Cargo.toml | 10 +++++++++
 tests/cargo-kani/mir-linker/expected   |  3 +++
 tests/cargo-kani/mir-linker/src/lib.rs | 29 ++++++++++++++++++++++++++
 3 files changed, 42 insertions(+)
 create mode 100644 tests/cargo-kani/mir-linker/Cargo.toml
 create mode 100644 tests/cargo-kani/mir-linker/expected
 create mode 100644 tests/cargo-kani/mir-linker/src/lib.rs

diff --git a/tests/cargo-kani/mir-linker/Cargo.toml b/tests/cargo-kani/mir-linker/Cargo.toml
new file mode 100644
index 000000000000..f00d4c687864
--- /dev/null
+++ b/tests/cargo-kani/mir-linker/Cargo.toml
@@ -0,0 +1,10 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+[package]
+name = "mir-linker"
+version = "0.1.0"
+edition = "2021"
+description = "Ensures that the mir-linker works accross crates"
+
+[dependencies]
+semver = "1.0"
diff --git a/tests/cargo-kani/mir-linker/expected b/tests/cargo-kani/mir-linker/expected
new file mode 100644
index 000000000000..2a5a5ac367ba
--- /dev/null
+++ b/tests/cargo-kani/mir-linker/expected
@@ -0,0 +1,3 @@
+Status: SUCCESS\
+Next is greater\
+in function check_version
diff --git a/tests/cargo-kani/mir-linker/src/lib.rs b/tests/cargo-kani/mir-linker/src/lib.rs
new file mode 100644
index 000000000000..a1514d454828
--- /dev/null
+++ b/tests/cargo-kani/mir-linker/src/lib.rs
@@ -0,0 +1,29 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! Dummy test to check --mir-linker runs on a cargo project.
+use semver::{BuildMetadata, Prerelease, Version};
+
+#[kani::proof]
+fn check_version() {
+    let next_major: u64 = kani::any();
+    let next_minor: u64 = kani::any();
+    kani::assume(next_major != 0 || next_minor != 0);
+
+    // Check whether this requirement matches version 1.2.3-alpha.1 (no)
+    let v0 = Version {
+        major: 0,
+        minor: 0,
+        patch: 0,
+        pre: Prerelease::EMPTY,
+        build: BuildMetadata::EMPTY,
+    };
+    let next = Version {
+        major: next_major,
+        minor: next_minor,
+        patch: 0,
+        pre: Prerelease::EMPTY,
+        build: BuildMetadata::EMPTY,
+    };
+    assert!(next > v0, "Next is greater");
+}