The Dafny scanner no longer recognizes lines beginning with # as prag…

…mas (#3452)

Fixes #3451

<small>By submitting this pull request, I confirm that my contribution
is made under the terms of the [MIT
license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>

---------

Co-authored-by: davidcok <[email protected]>
Co-authored-by: Fabio Madge <[email protected]>
Co-authored-by: Aaron Tomb <[email protected]>
Co-authored-by: Remy Willems <[email protected]>
Co-authored-by: Mikaël Mayer <[email protected]>
Co-authored-by: stefan-aws <[email protected]>
Co-authored-by: Aaron Tomb <[email protected]>
Co-authored-by: Alex Chew <[email protected]>

Source/DafnyCore/Coco/Scanner.frame

@@ -408,7 +408,10 @@ public class Scanner {
         if (ch == '\r' && buffer.Peek() != '\n') ch = EOL;
         if (ch == EOL) {
           line++; col = 0;
-        } else if (ch == '#' && col == 1) {
+        } else if (false && ch == '#' && col == 1) {
+          // This block of code implements the scanner recognizing line pragmas (#line) that reset the line number and filename.
+          // The pragma syntax can interfere with otherwise legal Dafny programs, so it is being disabled.
+          // Turn it back on by removing the 'false' in the condition, or perhaps by introducing a test of an option.
           int prLine = line;
           int prColumn = 0;
 

Test/git-issues/git-issue-3451/git-issue-3451.dfy

@@ -0,0 +1,10 @@
+// RUN: %exits-with 2 %baredafny resolve --use-basename-for-filename "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+// The #line should no longer be special
+const s := @"
+#line 5     
+"
+const k = 6  // error
+
+

Test/git-issues/git-issue-3451/git-issue-3451.dfy.expect

@@ -0,0 +1,2 @@
+git-issue-3451.dfy(8,10): Error: a const field should be initialized using ':=', not '='
+1 parse errors detected in git-issue-3451.dfy

Test/git-issues/git-issue-3451/git-issue-3451a.dfy

@@ -0,0 +1,8 @@
+// RUN: %exits-with 2 %baredafny resolve --use-basename-for-filename "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+// The #line should no longer be special
+#line Q     
+#zzzz
+
+

Test/git-issues/git-issue-3451/git-issue-3451a.dfy.expect

@@ -0,0 +1,3 @@
+git-issue-3451a.dfy(1,0): Warning: File contains no code
+git-issue-3451a.dfy(5,0): Error: this symbol not expected in Dafny
+1 parse errors detected in git-issue-3451a.dfy

docs/dev/news/3452.fix

@@ -0,0 +1 @@
+The Dafny scanner no longer treats lines beginning with # (even those in strings) as pragmas.