From 8b044446d4a4de759dd82c1e48a53b742eb46f96 Mon Sep 17 00:00:00 2001 From: Fabio Madge Date: Fri, 19 Jul 2024 22:39:27 +0200 Subject: [PATCH] fix: Crash when compiling an empty source file while including testing code --- .../AST/Statements/Assignment/AssignStmt.cs | 16 +++++++++------- .../DafnyCore/Rewriters/RunAllTestsMainMethod.cs | 2 +- .../LitTest/git-issues/git-issue-5637.dfy | 2 ++ .../LitTest/git-issues/git-issue-5637.dfy.expect | 7 +++++++ docs/dev/news/5638.fix | 1 + 5 files changed, 20 insertions(+), 8 deletions(-) create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5637.dfy create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5637.dfy.expect create mode 100644 docs/dev/news/5638.fix diff --git a/Source/DafnyCore/AST/Statements/Assignment/AssignStmt.cs b/Source/DafnyCore/AST/Statements/Assignment/AssignStmt.cs index 09f93ed194a..6bb7c994880 100644 --- a/Source/DafnyCore/AST/Statements/Assignment/AssignStmt.cs +++ b/Source/DafnyCore/AST/Statements/Assignment/AssignStmt.cs @@ -17,13 +17,15 @@ void ObjectInvariant() { public override IToken Tok { get { - var previous = Rhs.StartToken.Prev; - // If there was a single assignment, report on the operator. - var singleAssignment = previous.val == ":="; - // If there was an implicit return assignment, report on the return. - var implicitAssignment = previous.val == "return"; - if (singleAssignment || implicitAssignment) { - return previous; + if (Rhs.StartToken.Prev is not null) { + var previous = Rhs.StartToken.Prev; + // If there was a single assignment, report on the operator. + var singleAssignment = previous.val == ":="; + // If there was an implicit return assignment, report on the return. + var implicitAssignment = previous.val == "return"; + if (singleAssignment || implicitAssignment) { + return previous; + } } return Rhs.StartToken; } diff --git a/Source/DafnyCore/Rewriters/RunAllTestsMainMethod.cs b/Source/DafnyCore/Rewriters/RunAllTestsMainMethod.cs index dcff4cd2e98..24415062a93 100644 --- a/Source/DafnyCore/Rewriters/RunAllTestsMainMethod.cs +++ b/Source/DafnyCore/Rewriters/RunAllTestsMainMethod.cs @@ -93,7 +93,7 @@ internal override void PreResolve(Program program) { /// } /// internal override void PostResolve(Program program) { - var tok = program.GetStartOfFirstFileToken(); + var tok = program.GetStartOfFirstFileToken() ?? Token.NoToken; List mainMethodStatements = new(); var idGenerator = new FreshIdGenerator(); diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5637.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5637.dfy new file mode 100644 index 00000000000..20f766e2cbc --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5637.dfy @@ -0,0 +1,2 @@ +// RUN: %translate cs --include-test-runner --allow-warnings %s > "%t" +// RUN: %diff "%s.expect" "%t" \ No newline at end of file diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5637.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5637.dfy.expect new file mode 100644 index 00000000000..b9c7e092eb2 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5637.dfy.expect @@ -0,0 +1,7 @@ +git-issue-5637.dfy(1,0): Warning: File contains no code + | +1 | // RUN: %translate cs --include-test-runner --allow-warnings %s > "%t" + | ^ + + +Dafny program verifier finished with 0 verified, 0 errors diff --git a/docs/dev/news/5638.fix b/docs/dev/news/5638.fix new file mode 100644 index 00000000000..a9766728ba7 --- /dev/null +++ b/docs/dev/news/5638.fix @@ -0,0 +1 @@ +Crash when compiling an empty source file while including testing code