cerc-io/solidity
11
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] Fix ICE in BMC function inlining

Browse Source
This commit is contained in:
Leonardo Alt
2020-08-05 11:47:25 +02:00
parent c03ca195ac
commit 8df8c6e14f
7 changed files with 38 additions and 6 deletions
Download Patch File Download Diff File Expand all files Collapse all files
libsolidity/formal/BMC.cpp
+1 -1
View File
@@ -61,7 +61,7 @@ void BMC::analyze(SourceUnit const& _source, map<ASTNode const*, set<Verificatio
m_context.setSolver(m_interface.get());
m_context.clear();
m_context.setAssertionAccumulation(true);
m_variableUsage.setFunctionInlining(true);
m_variableUsage.setFunctionInlining(shouldInlineFunctionCall);
_source.accept(*this);
libsolidity/formal/CHC.cpp
-1
View File
@@ -82,7 +82,6 @@ void CHC::analyze(SourceUnit const& _source)
}
m_context.clear();
m_context.setAssertionAccumulation(false);
m_variableUsage.setFunctionInlining(false);
resetSourceAnalysis();
libsolidity/formal/VariableUsage.cpp
+2 -2
View File
@@ -60,8 +60,8 @@ void VariableUsage::endVisit(IndexAccess const& _indexAccess)
void VariableUsage::endVisit(FunctionCall const& _funCall)
{
if (m_inlineFunctionCalls)
if (auto const& funDef = SMTEncoder::functionCallToDefinition(_funCall))
if (m_inlineFunctionCalls(_funCall))
if (auto funDef = SMTEncoder::functionCallToDefinition(_funCall))
{
solAssert(funDef, "");
if (find(m_callStack.begin(), m_callStack.end(), funDef) == m_callStack.end())
libsolidity/formal/VariableUsage.h
+2 -2
View File
@@ -36,7 +36,7 @@ public:
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; }
void setFunctionInlining(std::function<bool(FunctionCall const&)> _inlineFunctionCalls) { m_inlineFunctionCalls = _inlineFunctionCalls; }
private:
void endVisit(Identifier const& _node) override;
@@ -54,7 +54,7 @@ private:
std::vector<CallableDeclaration const*> m_callStack;
CallableDeclaration const* m_lastCall = nullptr;
bool m_inlineFunctionCalls = false;
std::function<bool(FunctionCall const&)> m_inlineFunctionCalls = [](FunctionCall const&) { return false; };
};
}