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 imports

Browse Source
This commit is contained in:
Leonardo Alt
2020-09-11 13:34:46 +02:00
parent 72f8a753a9
commit 23ee011c56
13 changed files with 195 additions and 72 deletions
Download Patch File Download Diff File Expand all files Collapse all files
libsolidity/formal/SMTEncoder.cpp
+9 -4
View File
@@ -133,10 +133,7 @@ bool SMTEncoder::visit(FunctionDefinition const& _function)
if (_function.isConstructor())
inlineConstructorHierarchy(dynamic_cast<ContractDefinition const&>(*_function.scope()));
// Base constructors' parameters should be set by explicit calls,
// but the most derived one needs to be initialized.
if (_function.scope() == m_currentContract)
initializeLocalVariables(_function);
initializeLocalVariables(_function);
_function.parameterList().accept(*this);
if (_function.returnParameterList())
@@ -2040,6 +2037,14 @@ vector<VariableDeclaration const*> SMTEncoder::stateVariablesIncludingInheritedA
return stateVariablesIncludingInheritedAndPrivate(dynamic_cast<ContractDefinition const&>(*_function.scope()));
}
SourceUnit const* SMTEncoder::sourceUnitContaining(Scopable const& _scopable)
{
for (auto const* s = &_scopable; s; s = dynamic_cast<Scopable const*>(s->scope()))
if (auto const* source = dynamic_cast<SourceUnit const*>(s->scope()))
return source;
solAssert(false, "");
}
void SMTEncoder::createReturnedExpressions(FunctionCall const& _funCall)
{
FunctionDefinition const* funDef = functionCallToDefinition(_funCall);