aboutsummaryrefslogtreecommitdiffstats
path: root/libsolidity
diff options
context:
space:
mode:
authorAlex Beregszaszi <alex@rtfs.hu>2018-07-25 18:08:47 +0800
committerGitHub <noreply@github.com>2018-07-25 18:08:47 +0800
commitae15b52d932dc7b186b6560e8d910106c5ca1043 (patch)
tree5a8f21252742006aef8777e6ee39c853ed3cbf83 /libsolidity
parent167fe7c3706ba19713cd5727b62e7f019ad664d6 (diff)
parentd30a6de94287a4bd34b4cec09d60018f1bff083c (diff)
downloaddexon-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
Diffstat (limited to 'libsolidity')
-rw-r--r--libsolidity/formal/SMTChecker.cpp10
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, "");