From 278372c13d611b829fbad6984a0a3951f0a11d99 Mon Sep 17 00:00:00 2001 From: Alex Beregszaszi Date: Tue, 24 Jul 2018 22:43:05 +0100 Subject: Add assert for both branches in mergeVariables in SMTChecker --- libsolidity/formal/SMTChecker.cpp | 1 + 1 file changed, 1 insertion(+) (limited to 'libsolidity') diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp index e2a51267..c992fd61 100644 --- a/libsolidity/formal/SMTChecker.cpp +++ b/libsolidity/formal/SMTChecker.cpp @@ -752,6 +752,7 @@ void SMTChecker::mergeVariables(vector const& _varia set 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, ""); -- cgit From d30a6de94287a4bd34b4cec09d60018f1bff083c Mon Sep 17 00:00:00 2001 From: Alex Beregszaszi Date: Tue, 24 Jul 2018 23:23:54 +0100 Subject: Add better warning on binary operation on non-integer types in SMT Checker --- libsolidity/formal/SMTChecker.cpp | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) (limited to 'libsolidity') diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp index c992fd61..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(*_op.annotation().commonType); smt::Expression left(expr(_op.leftExpression())); smt::Expression right(expr(_op.rightExpression())); -- cgit