cerc-io/solidity
16
0
Fork 0
mirror of https://github.com/ethereum/solidity synced 2023-10-03 13:03:40 +00:00
Code Issues Actions Packages Projects Releases Wiki Activity

Merge pull request #4565 from ethereum/smt-stringutils-crash

Browse Source 
Add assert for both branches in mergeVariables in SMTChecker
This commit is contained in:
Alex Beregszaszi 2018-07-25 11:08:47 +01:00 committed by GitHub
commit ae15b52d93
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
1 changed files with 9 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

10
libsolidity/formal/SMTChecker.cpp
View File

@ -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, "");