SMT2 back-end: report error when invoking solver fails #8378
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
tautschnig
requested review from
kroening,
martin-cs,
peterschrammel and
TGWDB
as code owners
Our previous attempt at reporting errors was dead code for `run` never returns a negative value. When the executable isn't found the return code was 1, which is also a legitimate return code when `z3` runs successfully. Thus, use emptiness of `stderr` output as the success criterion, and propagate the messages produced by `run` on stderr to the error-logging output. Fixes: diffblue#8362
tautschnig
force-pushed
the
bugfixes/smt2-error-8362
branch
from
2409536
to
7fd93be
Compare
Codecov ReportAttention: Patch coverage is
Additional details and impacted files@@ Coverage Diff @@
## develop #8378 +/- ##
===========================================
- Coverage 78.35% 78.34% -0.01%
===========================================
Files 1726 1726
Lines 188424 188443 +19
Branches 18248 18248
===========================================
- Hits 147631 147630 -1
- Misses 40793 40813 +20 ☔ View full report in Codecov by Sentry. |
|
Thanks for this one. Have you tested it in the three obvious use cases:
|
|
OK... build this branch and tried it on the command-line. Issues:
|
|
I tried this using cbmc-starter-kit and running the tools with litani. With no Z3 installed, the run ends with: so nothing there about Z3 missing. Secondly, no "report" directory has been created, so nothing to find there in HTML either. The error messages does appear in logs/result.xml but buried on line 45 of a 6000 line file. |
|
We should likely work on the starter kit to do a better job at testing for dependencies and extracting useful information. This PR enables such work by making CBMC present the information rather than hiding it. |
kroening
reviewed
Jul 12, 2024
| @@ -135,13 +137,14 @@ decision_proceduret::resultt smt2_dect::dec_solve(const exprt &assumption) | |||
| UNREACHABLE; | |||
| } | |||
|
|
|||
| int res = | |||
| run(argv[0], argv, stdin_filename, temp_file_stdout(), temp_file_stderr()); | |||
| run(argv[0], argv, stdin_filename, temp_file_stdout(), temp_file_stderr()); | |||
There was a problem hiding this comment.
Should run not rather return a proper result?
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
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.
Our previous attempt at reporting errors was dead code for
runnever returns a negative value. When the executable isn't found the return code was 1, else failures will depend on the solver's return code. Also, propagate the messages produced byrunon stderr to the error-logging output.Fixes: #8362