From 63773cdbfbf9641fff21af5db9f436c6e28aaa7c Mon Sep 17 00:00:00 2001
From: "Brian R. Murphy" <132495859+brmataptos@users.noreply.github.com>
Date: Mon, 17 Jun 2024 18:58:55 -0700
Subject: [PATCH] add tests for #13737

---
 .../noverify/function_with_spec.exp           | 13 +++++++++++++
 .../noverify/function_with_spec.move          | 19 +++++++++++++++++++
 .../verify/function_with_spec.exp             | 10 ++++++++++
 .../verify/function_with_spec.move            | 19 +++++++++++++++++++
 4 files changed, 61 insertions(+)
 create mode 100644 third_party/move/move-compiler-v2/tests/more-v1/verification/noverify/function_with_spec.exp
 create mode 100644 third_party/move/move-compiler-v2/tests/more-v1/verification/noverify/function_with_spec.move
 create mode 100644 third_party/move/move-compiler-v2/tests/more-v1/verification/verify/function_with_spec.exp
 create mode 100644 third_party/move/move-compiler-v2/tests/more-v1/verification/verify/function_with_spec.move

diff --git a/third_party/move/move-compiler-v2/tests/more-v1/verification/noverify/function_with_spec.exp b/third_party/move/move-compiler-v2/tests/more-v1/verification/noverify/function_with_spec.exp
new file mode 100644
index 0000000000000..8813dd56cc765
--- /dev/null
+++ b/third_party/move/move-compiler-v2/tests/more-v1/verification/noverify/function_with_spec.exp
@@ -0,0 +1,13 @@
+
+Diagnostics:
+error: unresolved spec target
+   ┌─ tests/more-v1/verification/noverify/function_with_spec.move:10:10
+   │
+10 │     spec bar {
+   │          ^^^
+
+error: unresolved spec target
+   ┌─ tests/more-v1/verification/noverify/function_with_spec.move:15:10
+   │
+15 │     spec baz {
+   │          ^^^
diff --git a/third_party/move/move-compiler-v2/tests/more-v1/verification/noverify/function_with_spec.move b/third_party/move/move-compiler-v2/tests/more-v1/verification/noverify/function_with_spec.move
new file mode 100644
index 0000000000000..4671968e37fd2
--- /dev/null
+++ b/third_party/move/move-compiler-v2/tests/more-v1/verification/noverify/function_with_spec.move
@@ -0,0 +1,19 @@
+// #[test_only] functions should be filtered out in non-test mode
+address 0x1234 {
+module M {
+    public fun foo() { }
+
+    #[verify_only]
+    public fun bar() { }
+
+    // This should not cause an error in either test- nor non-test-mode.
+    spec bar {
+        aborts_if false;
+    }
+
+    // This should always cause an error due to typo.
+    spec baz {
+        aborts_if false;
+    }
+}
+}
diff --git a/third_party/move/move-compiler-v2/tests/more-v1/verification/verify/function_with_spec.exp b/third_party/move/move-compiler-v2/tests/more-v1/verification/verify/function_with_spec.exp
new file mode 100644
index 0000000000000..81708f74de71f
--- /dev/null
+++ b/third_party/move/move-compiler-v2/tests/more-v1/verification/verify/function_with_spec.exp
@@ -0,0 +1,10 @@
+
+Diagnostics:
+error: unresolved spec target
+   ┌─ tests/more-v1/verification/verify/function_with_spec.move:15:10
+   │
+15 │     spec baz {
+   │          ^^^
+
+
+============ bytecode verification succeeded ========
diff --git a/third_party/move/move-compiler-v2/tests/more-v1/verification/verify/function_with_spec.move b/third_party/move/move-compiler-v2/tests/more-v1/verification/verify/function_with_spec.move
new file mode 100644
index 0000000000000..4671968e37fd2
--- /dev/null
+++ b/third_party/move/move-compiler-v2/tests/more-v1/verification/verify/function_with_spec.move
@@ -0,0 +1,19 @@
+// #[test_only] functions should be filtered out in non-test mode
+address 0x1234 {
+module M {
+    public fun foo() { }
+
+    #[verify_only]
+    public fun bar() { }
+
+    // This should not cause an error in either test- nor non-test-mode.
+    spec bar {
+        aborts_if false;
+    }
+
+    // This should always cause an error due to typo.
+    spec baz {
+        aborts_if false;
+    }
+}
+}