diff options
| author | chriseth <chris@ethereum.org> | 2017-07-14 03:06:29 +0800 |
|---|---|---|
| committer | chriseth <chris@ethereum.org> | 2017-08-23 23:37:35 +0800 |
| commit | 1e05ebe50e0530beb62c96fc1112e935a5b11473 (patch) | |
| tree | 922b4aa1cb0d862d6c744e63243dfd4ef47ff869 /libsolidity/formal/SMTChecker.cpp | |
| parent | 9ac2ac14c1819be2341c6947245bf63b02795528 (diff) | |
| download | dexon-solidity-1e05ebe50e0530beb62c96fc1112e935a5b11473.tar.gz dexon-solidity-1e05ebe50e0530beb62c96fc1112e935a5b11473.tar.zst dexon-solidity-1e05ebe50e0530beb62c96fc1112e935a5b11473.zip | |
Refactor Z3 read callback.
Diffstat (limited to 'libsolidity/formal/SMTChecker.cpp')
| -rw-r--r-- | libsolidity/formal/SMTChecker.cpp | 27 |
1 files changed, 24 insertions, 3 deletions
diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp index a8ad60ed..c2f5c56d 100644 --- a/libsolidity/formal/SMTChecker.cpp +++ b/libsolidity/formal/SMTChecker.cpp @@ -17,7 +17,11 @@ #include <libsolidity/formal/SMTChecker.h> +#ifdef HAVE_Z3 +#include <libsolidity/formal/Z3Interface.h> +#else #include <libsolidity/formal/SMTLib2Interface.h> +#endif #include <libsolidity/interface/ErrorReporter.h> @@ -25,10 +29,15 @@ using namespace std; using namespace dev; using namespace dev::solidity; -SMTChecker::SMTChecker(ErrorReporter& _errorReporter, ReadFile::Callback const& _readFileCallback): +SMTChecker::SMTChecker(ErrorReporter& _errorReporter, ReadCallback::Callback const& _readFileCallback): +#ifdef HAVE_Z3 + m_interface(make_shared<smt::Z3Interface>()), +#else m_interface(make_shared<smt::SMTLib2Interface>(_readFileCallback)), +#endif m_errorReporter(_errorReporter) { + (void)_readFileCallback; } void SMTChecker::analyze(SourceUnit const& _source) @@ -36,7 +45,7 @@ void SMTChecker::analyze(SourceUnit const& _source) bool pragmaFound = false; for (auto const& node: _source.nodes()) if (auto const* pragma = dynamic_cast<PragmaDirective const*>(node.get())) - if (pragma->literals()[0] == "checkAssertionsZ3") + if (pragma->literals()[0] == "checkAssertions") pragmaFound = true; if (pragmaFound) { @@ -345,7 +354,19 @@ void SMTChecker::checkCondition( } smt::CheckResult result; vector<string> values; - tie(result, values) = m_interface->check(expressionsToEvaluate); + try + { + tie(result, values) = m_interface->check(expressionsToEvaluate); + } + catch (smt::SolverError const& _e) + { + string description("Error querying SMT solver"); + if (_e.comment()) + description += ": " + *_e.comment(); + m_errorReporter.warning(_location, description); + return; + } + switch (result) { case smt::CheckResult::SAT: |