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

Merge pull request #7650 from ethereum/develop

Browse Source 
Merge develop into develop_060
This commit is contained in:
chriseth
2019-11-06 21:56:55 +01:00
committed by GitHub
parent d4354a47b7 efeee15d32
commit 21e65076b3
30 changed files with 1081 additions and 135 deletions
Download Patch File Download Diff File Expand all files Collapse all files
libsolidity/formal/SMTEncoder.cpp
+37 -4
View File
@@ -36,12 +36,37 @@ SMTEncoder::SMTEncoder(smt::EncodingContext& _context):
bool SMTEncoder::visit(ContractDefinition const& _contract)
{
solAssert(m_currentContract == nullptr, "");
m_currentContract = &_contract;
solAssert(m_currentContract, "");
initializeStateVariables(_contract);
for (auto const& node: _contract.subNodes())
if (!dynamic_pointer_cast<FunctionDefinition>(node))
node->accept(*this);
return true;
vector<FunctionDefinition const*> resolvedFunctions = _contract.definedFunctions();
for (auto const& base: _contract.annotation().linearizedBaseContracts)
for (auto const& baseFunction: base->definedFunctions())
{
if (baseFunction->isConstructor())
continue;
bool overridden = false;
for (auto const& function: resolvedFunctions)
if (
function->name() == baseFunction->name() &&
FunctionType(*function).asCallableFunction(false)->
hasEqualParameterTypes(*FunctionType(*baseFunction).asCallableFunction(false))
)
{
overridden = true;
break;
}
if (!overridden)
resolvedFunctions.push_back(baseFunction);
}
for (auto const& function: resolvedFunctions)
function->accept(*this);
return false;
}
void SMTEncoder::endVisit(ContractDefinition const& _contract)
@@ -512,6 +537,14 @@ void SMTEncoder::endVisit(FunctionCall const& _funCall)
}
}
void SMTEncoder::initContract(ContractDefinition const& _contract)
{
solAssert(m_currentContract == nullptr, "");
m_currentContract = &_contract;
initializeStateVariables(_contract);
}
void SMTEncoder::initFunction(FunctionDefinition const& _function)
{
solAssert(m_callStack.empty(), "");