diff options
| -rw-r--r-- | libsolidity/formal/SMTChecker.cpp | 4 | ||||
| -rw-r--r-- | libsolidity/formal/SMTChecker.h | 5 | ||||
| -rw-r--r-- | libsolidity/interface/CompilerStack.cpp | 2 | ||||
| -rw-r--r-- | libsolidity/parsing/Scanner.h | 7 |
4 files changed, 15 insertions, 3 deletions
diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp index 51b310ae..cc580021 100644 --- a/libsolidity/formal/SMTChecker.cpp +++ b/libsolidity/formal/SMTChecker.cpp @@ -37,9 +37,10 @@ SMTChecker::SMTChecker(ErrorReporter& _errorReporter, ReadCallback::Callback con { } -void SMTChecker::analyze(SourceUnit const& _source) +void SMTChecker::analyze(SourceUnit const& _source, shared_ptr<Scanner> const& _scanner) { m_variableUsage = make_shared<VariableUsage>(_source); + m_scanner = _scanner; if (_source.annotation().experimentalFeatures.count(ExperimentalFeature::SMTChecker)) _source.accept(*this); } @@ -753,6 +754,7 @@ void SMTChecker::checkCondition( vector<string> expressionNames; if (m_functionPath.size()) { + solAssert(m_scanner, ""); if (_additionalValue) { expressionsToEvaluate.emplace_back(*_additionalValue); diff --git a/libsolidity/formal/SMTChecker.h b/libsolidity/formal/SMTChecker.h index 376b73fd..a7f955dd 100644 --- a/libsolidity/formal/SMTChecker.h +++ b/libsolidity/formal/SMTChecker.h @@ -25,6 +25,8 @@ #include <libsolidity/interface/ReadFile.h> +#include <libsolidity/parsing/Scanner.h> + #include <unordered_map> #include <string> #include <vector> @@ -42,7 +44,7 @@ class SMTChecker: private ASTConstVisitor public: SMTChecker(ErrorReporter& _errorReporter, ReadCallback::Callback const& _readCallback); - void analyze(SourceUnit const& _sources); + void analyze(SourceUnit const& _sources, std::shared_ptr<Scanner> const& _scanner); private: // TODO: Check that we do not have concurrent reads and writes to a variable, @@ -193,6 +195,7 @@ private: std::unordered_map<std::string, std::shared_ptr<SymbolicVariable>> m_specialVariables; std::vector<smt::Expression> m_pathConditions; ErrorReporter& m_errorReporter; + std::shared_ptr<Scanner> m_scanner; /// Stores the current path of function calls. std::vector<FunctionDefinition const*> m_functionPath; diff --git a/libsolidity/interface/CompilerStack.cpp b/libsolidity/interface/CompilerStack.cpp index 7aa0faa7..441c7897 100644 --- a/libsolidity/interface/CompilerStack.cpp +++ b/libsolidity/interface/CompilerStack.cpp @@ -284,7 +284,7 @@ bool CompilerStack::analyze() { SMTChecker smtChecker(m_errorReporter, m_smtQuery); for (Source const* source: m_sourceOrder) - smtChecker.analyze(*source->ast); + smtChecker.analyze(*source->ast, source->scanner); } } catch(FatalError const&) diff --git a/libsolidity/parsing/Scanner.h b/libsolidity/parsing/Scanner.h index 02e0553f..14eeb66e 100644 --- a/libsolidity/parsing/Scanner.h +++ b/libsolidity/parsing/Scanner.h @@ -162,6 +162,13 @@ public: /// Do only use in error cases, they are quite expensive. std::string lineAtPosition(int _position) const { return m_source.lineAtPosition(_position); } std::tuple<int, int> translatePositionToLineColumn(int _position) const { return m_source.translatePositionToLineColumn(_position); } + std::string sourceAt(SourceLocation const& _location) const + { + solAssert(!_location.isEmpty(), ""); + solAssert(m_sourceName && _location.sourceName, ""); + solAssert(*m_sourceName == *_location.sourceName, ""); + return m_source.source().substr(_location.start, _location.end - _location.start); + } ///@} private: |