Added missing tests

dafny-lang · Oct 10, 2024 · 53b2a01 · 53b2a01
1 parent 09a845d
commit 53b2a01
Show file tree

Hide file tree

Showing 2 changed files with 14 additions and 0 deletions.
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/at-attributes/at-attributes-typos0.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/at-attributes/at-attributes-typos0.dfy
@@ -0,0 +1,11 @@
+// RUN: %exits-with -any %resolve "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+// Attributes on top-level declarations
+
+@Option("--function-syntax:3") // Should be Options
+module SimpleLinearModule {
+}
+
+function OtherUnresolvedfunction(): string {
+  3
+}
diff --git a/...IntegrationTests/TestFiles/LitTests/LitTest/at-attributes/at-attributes-typos0.dfy.expect b/...IntegrationTests/TestFiles/LitTests/LitTest/at-attributes/at-attributes-typos0.dfy.expect
@@ -0,0 +1,3 @@
+at-attributes-typos0.dfy(5,1): Error: unresolved identifier: Option
+at-attributes-typos0.dfy(6,7): Error: not resolving module '_module' because there were errors in resolving its nested module 'SimpleLinearModule'
+2 resolution/type errors detected in at-attributes-typos0.dfy