Error handling cleanup in solvers/smt2#2963
Conversation
e5b5a69 to
6c4e483
Compare
allredj
left a comment
There was a problem hiding this comment.
Passed Diffblue compatibility checks (cbmc commit: 6c4e483).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/85042148
tautschnig
left a comment
There was a problem hiding this comment.
Mostly small issues; some of my comments repeat a couple of times, which really begs the question whether such code should be factored out.
src/util/arith_tools.h
Outdated
| /// Convert an mp_integer to integral type Target | ||
| /// An invariant with fail with message "Bad conversion" if conversion | ||
| /// is not possible. | ||
| /// An invariant with fail if the conversion is not possible. |
There was a problem hiding this comment.
Not actually your fault, but as you are touching this line: s/with/will/
src/util/arith_tools.h
Outdated
| /// Convert an expression to integral type Target | ||
| /// An invariant with fail with message "Bad conversion" if conversion | ||
| /// is not possible. | ||
| /// An invariant with fail if the conversion is not possible. |
There was a problem hiding this comment.
As above: s/with/will/
src/solvers/smt2/smt2_conv.cpp
Outdated
| mp_integer i; | ||
| if(to_integer(expr.op1(), i)) | ||
| INVALIDEXPR("byte_update takes constant as second parameter"); | ||
| mp_integer i = numeric_cast_v<mp_integer>(expr.op1()); |
There was a problem hiding this comment.
Use .offset() instead of .op1()
src/solvers/smt2/smt2_conv.cpp
Outdated
| { | ||
| irep_idt id=expr.get(ID_identifier); | ||
| DATA_INVARIANT(!id.empty(), "smt2_symbol must have identifier"); | ||
| irep_idt id = to_smt2_symbol(expr).get_identifier(); |
There was a problem hiding this comment.
While at it: const irep_idt &id
src/solvers/smt2/smt2_conv.cpp
Outdated
| assert(datatype_map.find(expr.type())!=datatype_map.end()); | ||
| INVARIANT( | ||
| datatype_map.find(bitnot_expr.type()) != datatype_map.end(), | ||
| "type shall have been mapped to Z3 datatype"); |
There was a problem hiding this comment.
Data types are currently only used when Z3 is used, but it now seems to be a standard SMTLIB feature. I've removed the invariants checking whether the element is in the map followed by a find() by a single call to at().
src/solvers/smt2/smt2_conv.cpp
Outdated
| assert(datatype_map.find(type)!=datatype_map.end()); | ||
| INVARIANT( | ||
| datatype_map.find(type) != datatype_map.end(), | ||
| "type should have been mapped to Z3 datatype"); |
src/solvers/smt2/smt2_conv.cpp
Outdated
| assert(datatype_map.find(type)!=datatype_map.end()); | ||
| INVARIANT( | ||
| datatype_map.find(type) != datatype_map.end(), | ||
| "type should have been mapped to Z3 datatype"); |
src/solvers/smt2/smt2_conv.cpp
Outdated
| assert(datatype_map.find(type)!=datatype_map.end()); | ||
| INVARIANT( | ||
| datatype_map.find(type) != datatype_map.end(), | ||
| "type should have been converted to Z3 datatype"); |
src/solvers/smt2/smt2_conv.cpp
Outdated
| assert(datatype_map.find(type)!=datatype_map.end()); | ||
| INVARIANT( | ||
| datatype_map.find(type) != datatype_map.end(), | ||
| "type should have been converted to Z3 datatype"); |
src/solvers/smt2/smt2_conv.cpp
Outdated
| assert(datatype_map.find(type)!=datatype_map.end()); | ||
| INVARIANT( | ||
| datatype_map.find(type) != datatype_map.end(), | ||
| "type should have been converted to Z3 datatype"); |
244316c to
b0f5db1
Compare
allredj
left a comment
There was a problem hiding this comment.
This PR failed Diffblue compatibility checks (cbmc commit: f88fcae).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/85440531
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.
Common spurious failures:
- the cbmc commit has disappeared in the mean time (e.g. in a force-push)
- the author is not in the list of contributors (e.g. first-time contributors).
allredj
left a comment
There was a problem hiding this comment.
This PR failed Diffblue compatibility checks (cbmc commit: 244316c).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/85443417
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.
Common spurious failures:
- the cbmc commit has disappeared in the mean time (e.g. in a force-push)
- the author is not in the list of contributors (e.g. first-time contributors).
allredj
left a comment
There was a problem hiding this comment.
Passed Diffblue compatibility checks (cbmc commit: b0f5db1).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/85448831
b0f5db1 to
0f6b06c
Compare
allredj
left a comment
There was a problem hiding this comment.
Passed Diffblue compatibility checks (cbmc commit: 0f6b06c).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/86324852
No description provided.