add tests for #13737

aptos-labs · Jul 11, 2024 · ea031cb · ea031cb
1 parent 5c84127
commit ea031cb
Show file tree

Hide file tree

Showing 4 changed files with 61 additions and 0 deletions.
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
@@ -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/...d_party/move/move-compiler-v2/tests/more-v1/verification/noverify/function_with_spec.move b/...d_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
@@ -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
@@ -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;
+    }
+}
+}