diff options
| author | Alex Beregszaszi <alex@rtfs.hu> | 2018-07-28 00:07:56 +0800 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-07-28 00:07:56 +0800 |
| commit | 2794a22d84d05c83bd6e9f57d16a9e66a662812f (patch) | |
| tree | c861a097b885416b67d2ef98f20ae9f91950756d /libsolidity/formal/SMTChecker.cpp | |
| parent | 5faa60e8834b5302f8d58f719c6962ed3affb50f (diff) | |
| parent | 55c1fb60b4ba60685262f332f2b197a7ef81d5b8 (diff) | |
| download | dexon-solidity-2794a22d84d05c83bd6e9f57d16a9e66a662812f.tar dexon-solidity-2794a22d84d05c83bd6e9f57d16a9e66a662812f.tar.gz dexon-solidity-2794a22d84d05c83bd6e9f57d16a9e66a662812f.tar.bz2 dexon-solidity-2794a22d84d05c83bd6e9f57d16a9e66a662812f.tar.lz dexon-solidity-2794a22d84d05c83bd6e9f57d16a9e66a662812f.tar.xz dexon-solidity-2794a22d84d05c83bd6e9f57d16a9e66a662812f.tar.zst dexon-solidity-2794a22d84d05c83bd6e9f57d16a9e66a662812f.zip | |
Merge pull request #4351 from ethereum/smt_portfolio
[SMTChecker] SMTPortfolio: use all SMT solvers available
Diffstat (limited to 'libsolidity/formal/SMTChecker.cpp')
| -rw-r--r-- | libsolidity/formal/SMTChecker.cpp | 22 |
1 files changed, 7 insertions, 15 deletions
diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp index 2623a2ba..109c8dbe 100644 --- a/libsolidity/formal/SMTChecker.cpp +++ b/libsolidity/formal/SMTChecker.cpp @@ -17,13 +17,7 @@ #include <libsolidity/formal/SMTChecker.h> -#ifdef HAVE_Z3 -#include <libsolidity/formal/Z3Interface.h> -#elif HAVE_CVC4 -#include <libsolidity/formal/CVC4Interface.h> -#else -#include <libsolidity/formal/SMTLib2Interface.h> -#endif +#include <libsolidity/formal/SMTPortfolio.h> #include <libsolidity/formal/SSAVariable.h> #include <libsolidity/formal/SymbolicIntVariable.h> @@ -39,16 +33,9 @@ using namespace dev; using namespace dev::solidity; SMTChecker::SMTChecker(ErrorReporter& _errorReporter, ReadCallback::Callback const& _readFileCallback): -#ifdef HAVE_Z3 - m_interface(make_shared<smt::Z3Interface>()), -#elif HAVE_CVC4 - m_interface(make_shared<smt::CVC4Interface>()), -#else - m_interface(make_shared<smt::SMTLib2Interface>(_readFileCallback)), -#endif + m_interface(make_shared<smt::SMTPortfolio>(_readFileCallback)), m_errorReporter(_errorReporter) { - (void)_readFileCallback; } void SMTChecker::analyze(SourceUnit const& _source) @@ -630,6 +617,9 @@ void SMTChecker::checkCondition( case smt::CheckResult::UNKNOWN: m_errorReporter.warning(_location, _description + " might happen here." + loopComment); break; + case smt::CheckResult::CONFLICTING: + m_errorReporter.warning(_location, "At least two SMT solvers provided conflicting answers. Results might not be sound."); + break; case smt::CheckResult::ERROR: m_errorReporter.warning(_location, "Error trying to invoke SMT solver."); break; @@ -657,6 +647,8 @@ void SMTChecker::checkBooleanNotConstant(Expression const& _condition, string co if (positiveResult == smt::CheckResult::ERROR || negatedResult == smt::CheckResult::ERROR) m_errorReporter.warning(_condition.location(), "Error trying to invoke SMT solver."); + else if (positiveResult == smt::CheckResult::CONFLICTING || negatedResult == smt::CheckResult::CONFLICTING) + m_errorReporter.warning(_condition.location(), "At least two SMT solvers provided conflicting answers. Results might not be sound."); else if (positiveResult == smt::CheckResult::SATISFIABLE && negatedResult == smt::CheckResult::SATISFIABLE) { // everything fine. |