cerc-io/solidity
16
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 #7849 from ethereum/smt_constructor_local_vars

Browse Source 
[SMTChecker] Fix constructors with local vars
This commit is contained in:
Leonardo 2019-11-29 17:46:29 +01:00 committed by GitHub
commit 2f6e006ea4
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
3 changed files with 53 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
libsolidity/formal/CHC.cpp
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
{

35
test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_mixed_chain_local_vars.sol Normal file
View File

@ -0,0 +1,35 @@
pragma experimental SMTChecker;
contract F {
uint a;
constructor() public {
uint f = 2;
a = f;
}
}
contract E is F {}
contract D is E {
constructor() public {
uint d = 3;
a = d;
}
}
contract C is D {}
contract B is C {
constructor() public {
uint b = 4;
a = b;
}
}
contract A is B {
constructor(uint x) public {
uint a1 = 4;
uint a2 = 5;
assert(a == a1);
assert(a == a2);
}
}
// ----
// Warning: (317-323): Unused function parameter. Remove or comment out the variable name to silence this warning.
// Warning: (385-400): Assertion violation happens here

13
test/libsolidity/smtCheckerTests/functions/constructor_this.sol Normal file
View File

@ -0,0 +1,13 @@
pragma experimental SMTChecker;
contract C {
function f() public pure {}
constructor() public {
C c = this;
c.f(); // this does not warn now, but should warn in the future
this.f();
(this).f();
}
}
// ----
// Warning: (204-208): "this" used in constructor. Note that external functions of a contract cannot be called while it is being constructed.
// Warning: (223-227): "this" used in constructor. Note that external functions of a contract cannot be called while it is being constructed.