Error handling cleanup in solvers/flattening 4 #2934
Conversation
danpoe
requested review from
kroening,
martin-cs,
peterschrammel,
pkesseli,
smowton and
tautschnig
as code owners
There was a problem hiding this comment.
Passed Diffblue compatibility checks (cbmc commit: 1161a36).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/84460365
| @@ -18,29 +18,33 @@ bvt boolbvt::convert_replication(const replication_exprt &expr) | |||
| return conversion_failed(expr); | |||
|
|
|||
| mp_integer times; | |||
| if(to_integer(expr.op0(), times)) | |||
| throw "replication takes constant as first parameter"; | |||
| bool error = to_integer(expr.op0(), times); | |||
There was a problem hiding this comment.
I'd just replace this with numeric_cast_v
|
|
||
| // we allow a constant as shift distance | ||
|
|
||
| if(expr.op1().is_constant()) | ||
| { | ||
| mp_integer i; | ||
| if(to_integer(expr.op1(), i)) | ||
| throw "convert_shift: failed to convert constant"; | ||
| bool error = to_integer(expr.op1(), i); |
| { | ||
| mp_integer from=string2integer(expr.op0().type().get_string(ID_from)); | ||
| mp_integer to=string2integer(expr.op0().type().get_string(ID_to)); | ||
| mp_integer from=string2integer(expr.op().type().get_string(ID_from)); |
danpoe
force-pushed
the
refactor/error-handling-solvers-flattening-from-boolbv-quantifier
branch
2 times, most recently
from
b9a4258 to
1fde831
Compare
There was a problem hiding this comment.
Passed Diffblue compatibility checks (cbmc commit: 1fde831).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/85546545
| assert(expr.op0().id()==ID_symbol); | ||
| DATA_INVARIANT( | ||
| expr.operands().size() == 2, | ||
| "quantifier expressions shall have two operands"); |
There was a problem hiding this comment.
I believe we have to_quantifier_expr by now, and that method should actually take a quantifier_exprt.
| @@ -203,6 +204,8 @@ bool instantiate_quantifier(exprt &expr, | |||
|
|
|||
| literalt boolbvt::convert_quantifier(const exprt &src) | |||
| { | |||
| PRECONDITION(src.id() == ID_forall || src.id() == ID_exists); | |||
There was a problem hiding this comment.
The method should take a quantifier_exprt
|
|
||
| bvt bv; | ||
| bv.resize(width); | ||
|
|
||
| std::size_t offset=0; | ||
| //std::size_t offset=0; |
danpoe
force-pushed
the
refactor/error-handling-solvers-flattening-from-boolbv-quantifier
branch
from
1fde831 to
f971997
Compare
There was a problem hiding this comment.
Passed Diffblue compatibility checks (cbmc commit: f971997).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/85672302
danpoe
force-pushed
the
refactor/error-handling-solvers-flattening-from-boolbv-quantifier
branch
from
f971997 to
213bfeb
Compare
There was a problem hiding this comment.
Passed Diffblue compatibility checks (cbmc commit: 213bfeb).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/85784112
Files boolbv_quantifier.cpp to boolbv_typecast.cpp
danpoe
force-pushed
the
refactor/error-handling-solvers-flattening-from-boolbv-quantifier
branch
from
213bfeb to
44503dd
Compare
There was a problem hiding this comment.
Passed Diffblue compatibility checks (cbmc commit: 44503dd).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/85871012
danpoe
deleted the
refactor/error-handling-solvers-flattening-from-boolbv-quantifier
branch
No description provided.