From 96b0c4c148c28a2cf6c3b794d20f63ca9f2f6631 Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Mon, 8 Jul 2019 11:15:15 +0200 Subject: [PATCH] [SMTChecker] New VariableUsage flag to inline functions --- libsolidity/formal/BMC.cpp | 1 + libsolidity/formal/VariableUsage.cpp | 8 ++++---- libsolidity/formal/VariableUsage.h | 5 +++++ 3 files changed, 10 insertions(+), 4 deletions(-) diff --git a/libsolidity/formal/BMC.cpp b/libsolidity/formal/BMC.cpp index 5e3f6c7ff..54241ce88 100644 --- a/libsolidity/formal/BMC.cpp +++ b/libsolidity/formal/BMC.cpp @@ -50,6 +50,7 @@ void BMC::analyze(SourceUnit const& _source, shared_ptr const& _scanner m_scanner = _scanner; m_context.clear(); + m_variableUsage.setFunctionInlining(true); _source.accept(*this); diff --git a/libsolidity/formal/VariableUsage.cpp b/libsolidity/formal/VariableUsage.cpp index 3f71d2ccf..59729be2a 100644 --- a/libsolidity/formal/VariableUsage.cpp +++ b/libsolidity/formal/VariableUsage.cpp @@ -57,10 +57,10 @@ void VariableUsage::endVisit(IndexAccess const& _indexAccess) void VariableUsage::endVisit(FunctionCall const& _funCall) { - /// TODO this should run only in the BMC case, not for Horn. - if (auto const& funDef = BMC::inlinedFunctionCallToDefinition(_funCall)) - if (find(m_callStack.begin(), m_callStack.end(), funDef) == m_callStack.end()) - funDef->accept(*this); + if (m_inlineFunctionCalls) + if (auto const& funDef = BMC::inlinedFunctionCallToDefinition(_funCall)) + if (find(m_callStack.begin(), m_callStack.end(), funDef) == m_callStack.end()) + funDef->accept(*this); } bool VariableUsage::visit(FunctionDefinition const& _function) diff --git a/libsolidity/formal/VariableUsage.h b/libsolidity/formal/VariableUsage.h index 83362d940..7985655ab 100644 --- a/libsolidity/formal/VariableUsage.h +++ b/libsolidity/formal/VariableUsage.h @@ -38,6 +38,9 @@ public: /// @param _outerCallstack the current callstack in the callers context. std::set touchedVariables(ASTNode const& _node, std::vector const& _outerCallstack); + /// Sets whether to inline function calls. + void setFunctionInlining(bool _inlineFunction) { m_inlineFunctionCalls = _inlineFunction; } + private: void endVisit(Identifier const& _node) override; void endVisit(IndexAccess const& _node) override; @@ -53,6 +56,8 @@ private: std::set m_touchedVariables; std::vector m_callStack; CallableDeclaration const* m_lastCall = nullptr; + + bool m_inlineFunctionCalls = false; }; }