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 constructors with local vars

Browse Source
This commit is contained in:
Leonardo Alt
2019-11-29 16:59:15 +01:00
parent 27097b3eca
commit c09da092d2
3 changed files with 53 additions and 3 deletions
Download Patch File Download Diff File Expand all files Collapse all files
libsolidity/formal/CHC.cpp
+5 -3
View File
@@ -215,9 +215,11 @@ void CHC::endVisit(FunctionDefinition const& _function)
// This is done in endVisit(ContractDefinition).
if (_function.isConstructor())
{
auto constructorExit = createBlock(&_function, "exit_");
connectBlocks(m_currentBlock, predicate(*constructorExit));
setCurrentBlock(*constructorExit);
auto constructorExit = createSymbolicBlock(interfaceSort(), "constructor_exit_" + to_string(_function.id()));
connectBlocks(m_currentBlock, predicate(*constructorExit, currentStateVariables()));
clearIndices(m_currentContract, m_currentFunction);
auto stateExprs = currentStateVariables();
setCurrentBlock(*constructorExit, &stateExprs);
}
else
{