From 791a1270e2136edc8cfb84483bbb856307f63552 Mon Sep 17 00:00:00 2001 From: David Cok Date: Fri, 3 Feb 2023 07:27:29 -0500 Subject: [PATCH] The Dafny scanner no longer recognizes lines beginning with # as pragmas (#3452) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Fixes #3451 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). --------- Co-authored-by: davidcok Co-authored-by: Fabio Madge Co-authored-by: Aaron Tomb Co-authored-by: Remy Willems Co-authored-by: Mikaël Mayer Co-authored-by: stefan-aws <120379523+stefan-aws@users.noreply.github.com> Co-authored-by: Aaron Tomb Co-authored-by: Alex Chew --- Source/DafnyCore/Coco/Scanner.frame | 5 ++++- Test/git-issues/git-issue-3451/git-issue-3451.dfy | 10 ++++++++++ .../git-issue-3451/git-issue-3451.dfy.expect | 2 ++ Test/git-issues/git-issue-3451/git-issue-3451a.dfy | 8 ++++++++ .../git-issue-3451/git-issue-3451a.dfy.expect | 3 +++ docs/dev/news/3452.fix | 1 + 6 files changed, 28 insertions(+), 1 deletion(-) create mode 100644 Test/git-issues/git-issue-3451/git-issue-3451.dfy create mode 100644 Test/git-issues/git-issue-3451/git-issue-3451.dfy.expect create mode 100644 Test/git-issues/git-issue-3451/git-issue-3451a.dfy create mode 100644 Test/git-issues/git-issue-3451/git-issue-3451a.dfy.expect create mode 100644 docs/dev/news/3452.fix diff --git a/Source/DafnyCore/Coco/Scanner.frame b/Source/DafnyCore/Coco/Scanner.frame index dcc846e9992..44ac84f1b72 100644 --- a/Source/DafnyCore/Coco/Scanner.frame +++ b/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; diff --git a/Test/git-issues/git-issue-3451/git-issue-3451.dfy b/Test/git-issues/git-issue-3451/git-issue-3451.dfy new file mode 100644 index 00000000000..eec2674936d --- /dev/null +++ b/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 + + diff --git a/Test/git-issues/git-issue-3451/git-issue-3451.dfy.expect b/Test/git-issues/git-issue-3451/git-issue-3451.dfy.expect new file mode 100644 index 00000000000..aac4a15421e --- /dev/null +++ b/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 diff --git a/Test/git-issues/git-issue-3451/git-issue-3451a.dfy b/Test/git-issues/git-issue-3451/git-issue-3451a.dfy new file mode 100644 index 00000000000..e9dde98f053 --- /dev/null +++ b/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 + + diff --git a/Test/git-issues/git-issue-3451/git-issue-3451a.dfy.expect b/Test/git-issues/git-issue-3451/git-issue-3451a.dfy.expect new file mode 100644 index 00000000000..813b6fa066a --- /dev/null +++ b/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 diff --git a/docs/dev/news/3452.fix b/docs/dev/news/3452.fix new file mode 100644 index 00000000000..3c9a1547ec0 --- /dev/null +++ b/docs/dev/news/3452.fix @@ -0,0 +1 @@ +The Dafny scanner no longer treats lines beginning with # (even those in strings) as pragmas.