add tests for #13737

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 {
+   │          ^^^

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;
+    }
+}
+}

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 ========

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;
+    }
+}
+}

third_party/move/move-compiler-v2/tests/unit_test/notest/function_with_spec.exp

@@ -0,0 +1,13 @@
+
+Diagnostics:
+error: unresolved spec target
+   ┌─ tests/unit_test/notest/function_with_spec.move:13:10
+   │
+13 │     spec bar {
+   │          ^^^
+
+error: unresolved spec target
+   ┌─ tests/unit_test/notest/function_with_spec.move:18:10
+   │
+18 │     spec baz {
+   │          ^^^

third_party/move/move-compiler-v2/tests/unit_test/notest/function_with_spec.move

@@ -0,0 +1,22 @@
+// #[test_only] functions should be filtered out in non-test mode
+address 0x1234 {
+module M {
+    public fun foo() { }
+
+    #[test]
+    public fun bar_test() { bar() }
+
+    #[test_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;
+    }
+}
+}

third_party/move/move-compiler-v2/tests/unit_test/test/function_with_spec.exp

@@ -0,0 +1,10 @@
+
+Diagnostics:
+error: unresolved spec target
+   ┌─ tests/unit_test/test/function_with_spec.move:18:10
+   │
+18 │     spec baz {
+   │          ^^^
+
+
+============ bytecode verification succeeded ========

third_party/move/move-compiler-v2/tests/unit_test/test/function_with_spec.move

@@ -0,0 +1,22 @@
+// #[test_only] functions should be filtered out in non-test mode
+address 0x1234 {
+module M {
+    public fun foo() { }
+
+    #[test]
+    public fun bar_test() { bar() }
+
+    #[test_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;
+    }
+}
+}