cerc-io/solidity
15
0
Fork 0
mirror of https://github.com/ethereum/solidity synced 2023-10-03 13:03:40 +00:00
Code Issues Actions Packages Projects Releases Wiki Activity

[SMTChecker] New VariableUsage flag to inline functions

Browse Source
This commit is contained in:
Leonardo Alt 2019-07-08 11:15:15 +02:00
parent 035fde2932
commit 96b0c4c148
3 changed files with 10 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
libsolidity/formal/BMC.cpp
View File

@ -50,6 +50,7 @@ void BMC::analyze(SourceUnit const& _source, shared_ptr<Scanner> const& _scanner
m_scanner = _scanner; m_scanner = _scanner;
m_context.clear(); m_context.clear();
m_variableUsage.setFunctionInlining(true);
_source.accept(*this); _source.accept(*this);

8
libsolidity/formal/VariableUsage.cpp
View File

@ -57,10 +57,10 @@ void VariableUsage::endVisit(IndexAccess const& _indexAccess)
void VariableUsage::endVisit(FunctionCall const& _funCall) void VariableUsage::endVisit(FunctionCall const& _funCall)
{ {
/// TODO this should run only in the BMC case, not for Horn. if (m_inlineFunctionCalls)
if (auto const& funDef = BMC::inlinedFunctionCallToDefinition(_funCall)) if (auto const& funDef = BMC::inlinedFunctionCallToDefinition(_funCall))
if (find(m_callStack.begin(), m_callStack.end(), funDef) == m_callStack.end()) if (find(m_callStack.begin(), m_callStack.end(), funDef) == m_callStack.end())
funDef->accept(*this); funDef->accept(*this);
} }
bool VariableUsage::visit(FunctionDefinition const& _function) bool VariableUsage::visit(FunctionDefinition const& _function)

5
libsolidity/formal/VariableUsage.h
View File

@ -38,6 +38,9 @@ public:
/// @param _outerCallstack the current callstack in the callers context. /// @param _outerCallstack the current callstack in the callers context.
std::set<VariableDeclaration const*> touchedVariables(ASTNode const& _node, std::vector<CallableDeclaration const*> const& _outerCallstack); std::set<VariableDeclaration const*> touchedVariables(ASTNode const& _node, std::vector<CallableDeclaration const*> const& _outerCallstack);
/// Sets whether to inline function calls.
void setFunctionInlining(bool _inlineFunction) { m_inlineFunctionCalls = _inlineFunction; }
private: private:
void endVisit(Identifier const& _node) override; void endVisit(Identifier const& _node) override;
void endVisit(IndexAccess const& _node) override; void endVisit(IndexAccess const& _node) override;
@ -53,6 +56,8 @@ private:
std::set<VariableDeclaration const*> m_touchedVariables; std::set<VariableDeclaration const*> m_touchedVariables;
std::vector<CallableDeclaration const*> m_callStack; std::vector<CallableDeclaration const*> m_callStack;
CallableDeclaration const* m_lastCall = nullptr; CallableDeclaration const* m_lastCall = nullptr;
bool m_inlineFunctionCalls = false;
}; };
} }