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] Split SMTChecker into SMTEncoder and BMC

Browse Source
This commit is contained in:
Leonardo Alt
2019-07-01 15:05:03 +02:00
parent b8dbf7d2a8
commit 3cb4ed83c1
11 changed files with 1319 additions and 920 deletions
Download Patch File Download Diff File Expand all files Collapse all files
libsolidity/formal/VariableUsage.cpp
+5 -3
View File
@@ -17,7 +17,8 @@
#include <libsolidity/formal/VariableUsage.h>
#include <libsolidity/formal/SMTChecker.h>
#include <libsolidity/formal/BMC.h>
#include <libsolidity/formal/SMTEncoder.h>
#include <algorithm>
@@ -48,7 +49,7 @@ void VariableUsage::endVisit(IndexAccess const& _indexAccess)
{
/// identifier.annotation().lValueRequested == false, that's why we
/// need to check that before.
auto identifier = dynamic_cast<Identifier const*>(SMTChecker::leftmostBase(_indexAccess));
auto identifier = dynamic_cast<Identifier const*>(SMTEncoder::leftmostBase(_indexAccess));
if (identifier)
checkIdentifier(*identifier);
}
@@ -56,7 +57,8 @@ void VariableUsage::endVisit(IndexAccess const& _indexAccess)
void VariableUsage::endVisit(FunctionCall const& _funCall)
{
if (auto const& funDef = SMTChecker::inlinedFunctionCallToDefinition(_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);
}