Skip to content

Commit

Permalink
fix: Avoid NPE when building a doo file with —no-verify (#5152)
Browse files Browse the repository at this point in the history
### 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.
  • Loading branch information
robin-aws authored Mar 6, 2024
1 parent 354aaeb commit 5ece05f
Show file tree
Hide file tree
Showing 3 changed files with 11 additions and 1 deletion.
3 changes: 2 additions & 1 deletion Source/DafnyCore/DooFile.cs
Original file line number Diff line number Diff line change
Expand Up @@ -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<string, object>();
foreach (var (option, _) in OptionChecks) {
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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 {
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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

0 comments on commit 5ece05f

Please sign in to comment.