SMT2 type checking for define-fun #3421
Conversation
kroening
commented
Nov 14, 2018
kroening
commented
- Each commit message has a non-empty body, explaining why the change was made.
- Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
- Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
- n/a My commit message includes data points confirming performance improvements (if claimed).
- My PR is restricted to a single feature or bugfix.
- White-space or formatting changes outside the feature-related changed lines are in commits of their own.
kroening
requested review from
martin-cs,
peterschrammel and
tautschnig
as code owners
kroening
force-pushed
the
smt2-fapp-type-checking
branch
3 times, most recently
from
d9c7b9e to
31eb34a
Compare
There was a problem hiding this comment.
✔️
Passed Diffblue compatibility checks (cbmc commit: 31eb34a).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/91490994
|
|
||
| ^EXIT=0$ | ||
| ^SIGNAL=0$ | ||
| ^line 5: type mismatch in function definition: expected `\(_ BitVec 16\)' but got `\(_ BitVec 8\)'$ |
There was a problem hiding this comment.
So the exit code is useless?
There was a problem hiding this comment.
Most solvers seem to do the "continued-execution" error handling from the SMT-LIB standard; yes, the exit code is then used for SAT/UNSAT only.
kroening
force-pushed
the
smt2-fapp-type-checking
branch
3 times, most recently
from
866350e to
9b0e043
Compare
src/solvers/smt2/smt2_parser.h
Outdated
| } | ||
|
|
||
| const typet type; | ||
|
|
There was a problem hiding this comment.
This blank line might (should) trip up the linter.
src/solvers/smt2/smt2_parser.h
Outdated
| public: | ||
| class smt2_format | ||
| { | ||
| public: |
There was a problem hiding this comment.
Nit pick: Maybe just make this a struct and remove the public as we do in some other places?
src/solvers/smt2/smt2_parser.h
Outdated
| @@ -80,6 +80,20 @@ class smt2_parsert:public smt2_tokenizert | |||
|
|
|||
| /// Apply typecast to unsignedbv to given expression | |||
| exprt cast_bv_to_unsigned(const exprt &); | |||
|
|
|||
| public: | |||
There was a problem hiding this comment.
Nit pick: maybe just move this chunk of code into the earlier public section rather than having multiple ones?
| rm Linking4/test.desc | ||
| rm Linking7/test.desc | ||
| rm Malloc17/test.desc | ||
| rm Malloc18/test.desc | ||
| rm Malloc19/test.desc | ||
| rm Malloc20/test.desc | ||
| rm Malloc21/test.desc |
There was a problem hiding this comment.
I am surprised that this is now causing more failures?
There was a problem hiding this comment.
To be expected: the solver is now less permissive than it used to be. These two tests indicate cases in which the back-end generates invalid SMT-LIB files.
kroening
force-pushed
the
smt2-fapp-type-checking
branch
from
9b0e043 to
40c0362
Compare
kroening
force-pushed
the
smt2-fapp-type-checking
branch
from
40c0362 to
be0c338
Compare
There was a problem hiding this comment.
✔️
Passed Diffblue compatibility checks (cbmc commit: be0c338).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/91783476
