diff options
Diffstat (limited to 'libsolidity/formal/SMTChecker.cpp')
| -rw-r--r-- | libsolidity/formal/SMTChecker.cpp | 20 |
1 files changed, 15 insertions, 5 deletions
diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp index 61cb110e..d4887a3d 100644 --- a/libsolidity/formal/SMTChecker.cpp +++ b/libsolidity/formal/SMTChecker.cpp @@ -345,14 +345,14 @@ void SMTChecker::endVisit(FunctionCall const& _funCall) solAssert(args.size() == 1, ""); solAssert(args[0]->annotation().type->category() == Type::Category::Bool, ""); checkCondition(!(expr(*args[0])), _funCall.location(), "Assertion violation"); - m_interface->addAssertion(smt::Expression::implies(currentPathConditions(), expr(*args[0]))); + addPathImpliedExpression(expr(*args[0])); } else if (funType.kind() == FunctionType::Kind::Require) { solAssert(args.size() == 1, ""); solAssert(args[0]->annotation().type->category() == Type::Category::Bool, ""); checkBooleanNotConstant(*args[0], "Condition is always $VALUE."); - m_interface->addAssertion(smt::Expression::implies(currentPathConditions(), expr(*args[0]))); + addPathImpliedExpression(expr(*args[0])); } } @@ -534,7 +534,7 @@ void SMTChecker::checkCondition( ) { m_interface->push(); - m_interface->addAssertion(currentPathConditions() && _condition); + addPathConjoinedExpression(_condition); vector<smt::Expression> expressionsToEvaluate; vector<string> expressionNames; @@ -606,12 +606,12 @@ void SMTChecker::checkBooleanNotConstant(Expression const& _condition, string co return; m_interface->push(); - m_interface->addAssertion(currentPathConditions() && expr(_condition)); + addPathConjoinedExpression(expr(_condition)); auto positiveResult = checkSatisifable(); m_interface->pop(); m_interface->push(); - m_interface->addAssertion(currentPathConditions() && !expr(_condition)); + addPathConjoinedExpression(!expr(_condition)); auto negatedResult = checkSatisifable(); m_interface->pop(); @@ -847,3 +847,13 @@ smt::Expression SMTChecker::currentPathConditions() return smt::Expression(true); return m_pathConditions.back(); } + +void SMTChecker::addPathConjoinedExpression(smt::Expression const& _e) +{ + m_interface->addAssertion(currentPathConditions() && _e); +} + +void SMTChecker::addPathImpliedExpression(smt::Expression const& _e) +{ + m_interface->addAssertion(smt::Expression::implies(currentPathConditions(), _e)); +} |