diff options
| author | Alex Beregszaszi <alex@rtfs.hu> | 2018-07-25 18:08:47 +0800 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-07-25 18:08:47 +0800 |
| commit | ae15b52d932dc7b186b6560e8d910106c5ca1043 (patch) | |
| tree | 5a8f21252742006aef8777e6ee39c853ed3cbf83 | |
| parent | 167fe7c3706ba19713cd5727b62e7f019ad664d6 (diff) | |
| parent | d30a6de94287a4bd34b4cec09d60018f1bff083c (diff) | |
| download | dexon-solidity-ae15b52d932dc7b186b6560e8d910106c5ca1043.tar.gz dexon-solidity-ae15b52d932dc7b186b6560e8d910106c5ca1043.tar.zst dexon-solidity-ae15b52d932dc7b186b6560e8d910106c5ca1043.zip | |
Merge pull request #4565 from ethereum/smt-stringutils-crash
Add assert for both branches in mergeVariables in SMTChecker
| -rw-r--r-- | libsolidity/formal/SMTChecker.cpp | 10 |
1 files changed, 9 insertions, 1 deletions
diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp index e2a51267..2623a2ba 100644 --- a/libsolidity/formal/SMTChecker.cpp +++ b/libsolidity/formal/SMTChecker.cpp @@ -429,7 +429,14 @@ void SMTChecker::arithmeticOperation(BinaryOperation const& _op) case Token::Div: { solAssert(_op.annotation().commonType, ""); - solAssert(_op.annotation().commonType->category() == Type::Category::Integer, ""); + if (_op.annotation().commonType->category() != Type::Category::Integer) + { + m_errorReporter.warning( + _op.location(), + "Assertion checker does not yet implement this operator on non-integer types." + ); + break; + } auto const& intType = dynamic_cast<IntegerType const&>(*_op.annotation().commonType); smt::Expression left(expr(_op.leftExpression())); smt::Expression right(expr(_op.rightExpression())); @@ -752,6 +759,7 @@ void SMTChecker::mergeVariables(vector<VariableDeclaration const*> const& _varia set<VariableDeclaration const*> uniqueVars(_variables.begin(), _variables.end()); for (auto const* decl: uniqueVars) { + solAssert(_countersEndTrue.count(decl) && _countersEndFalse.count(decl), ""); int trueCounter = _countersEndTrue.at(decl).index(); int falseCounter = _countersEndFalse.at(decl).index(); solAssert(trueCounter != falseCounter, ""); |