fix: Avoid NPE when building a doo file with —no-verify #5152
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
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.By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.