diff options
| -rw-r--r-- | libsolidity/formal/SMTChecker.cpp | 20 | ||||
| -rw-r--r-- | libsolidity/formal/SMTChecker.h | 4 |
2 files changed, 19 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)); +} diff --git a/libsolidity/formal/SMTChecker.h b/libsolidity/formal/SMTChecker.h index 7f990b97..539221cc 100644 --- a/libsolidity/formal/SMTChecker.h +++ b/libsolidity/formal/SMTChecker.h @@ -152,6 +152,10 @@ private: void popPathCondition(); /// Returns the conjunction of all path conditions or True if empty smt::Expression currentPathConditions(); + /// Conjoin the current path conditions with the given parameter and add to the solver + void addPathConjoinedExpression(smt::Expression const& _e); + /// Add to the solver: the given expression implied by the current path conditions + void addPathImpliedExpression(smt::Expression const& _e); std::shared_ptr<smt::SolverInterface> m_interface; std::shared_ptr<VariableUsage> m_variableUsage; |