From 5ece05f6f7275bd41880e085464c9c24df73d182 Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Wed, 6 Mar 2024 11:37:07 -0800 Subject: [PATCH] =?UTF-8?q?fix:=20Avoid=20NPE=20when=20building=20a=20doo?= =?UTF-8?q?=20file=20with=20=E2=80=94no-verify=20(#5152)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit ### Description Fixes #5143. ### How has this been tested? Added this case to `separate-verification/app.dfy`. `separate-verification/assumptions.dfy` SHOULD have caught this regression, but unfortunately the command that triggers the exception uses `!` to expect a non-zero exit code, and LIT test commands usually only redirect stdout to a file to diff against the expected output, so the extra stderr output with the exception trace is lost. --- Source/DafnyCore/DooFile.cs | 3 ++- .../LitTests/LitTest/separate-verification/app.dfy | 6 ++++++ .../LitTests/LitTest/separate-verification/app.dfy.expect | 3 +++ 3 files changed, 11 insertions(+), 1 deletion(-) diff --git a/Source/DafnyCore/DooFile.cs b/Source/DafnyCore/DooFile.cs index d04d884231c..3d31b95d1dc 100644 --- a/Source/DafnyCore/DooFile.cs +++ b/Source/DafnyCore/DooFile.cs @@ -39,7 +39,8 @@ public ManifestData(DafnyOptions options) { DafnyVersion = options.VersionNumber; SolverIdentifier = options.SolverIdentifier; - SolverVersion = options.SolverVersion.ToString(); + // options.SolverVersion may be null (if --no-verify is used for example) + SolverVersion = options.SolverVersion?.ToString(); Options = new Dictionary(); foreach (var (option, _) in OptionChecks) { diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/separate-verification/app.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/separate-verification/app.dfy index 49d9c150012..def0661599a 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/separate-verification/app.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/separate-verification/app.dfy @@ -9,6 +9,9 @@ // RUN: %baredafny build %args -t:lib --boogie /vcsSplitOnEveryAssert %S/Inputs/wrappers.dfy // RUN: %baredafny build %args -t:lib --boogie /vcsSplitOnEveryAssert %S/Inputs/seq.dfy --library %S/Inputs/wrappers.doo >> %t +// RUN: %baredafny build %args -t:lib --no-verify %S/Inputs/wrappers.dfy +// RUN: %baredafny build %args -t:lib --no-verify %S/Inputs/seq.dfy --library %S/Inputs/wrappers.doo >> %t + // Supported: mismatching irrelevant options // RUN: %baredafny build %args -t:lib --function-syntax:3 %S/Inputs/wrappers3.dfy @@ -22,6 +25,9 @@ // RUN: %baredafny build %args -t:lib --boogie /vcsLoad:2 %S/Inputs/wrappers.dfy // RUN: ! %baredafny build %args -t:lib %S/Inputs/seq.dfy --library %S/Inputs/wrappers.doo >> %t +// RUN: %baredafny build %args -t:lib --no-verify %S/Inputs/wrappers.dfy +// RUN: ! %baredafny build %args -t:lib %S/Inputs/seq.dfy --library %S/Inputs/wrappers.doo >> %t + // RUN: %diff "%s.expect" %t module App { diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/separate-verification/app.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/separate-verification/app.dfy.expect index 6db0240a124..50c7835bf5a 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/separate-verification/app.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/separate-verification/app.dfy.expect @@ -8,6 +8,9 @@ Dafny program verifier finished with 1 verified, 0 errors Dafny program verifier finished with 2 verified, 0 errors +Dafny program verifier did not attempt verification + Dafny program verifier finished with 2 verified, 0 errors CLI: Error: cannot load wrappers.doo: --unicode-char is set locally to False, but the library was built with True CLI: Error: cannot load wrappers.doo: --boogie is set locally to [], but the library was built with [/vcsLoad:2] +CLI: Error: cannot load wrappers.doo: --no-verify is set locally to False, but the library was built with True