diff options
author | Leonardo Alt <leo@ethereum.org> | 2018-12-21 01:11:20 +0800 |
---|---|---|
committer | Leonardo Alt <leo@ethereum.org> | 2019-01-21 19:58:40 +0800 |
commit | 7f8ceaadab0c265674b591aa50cfeb8910628b9f (patch) | |
tree | 2deda16f70a2a8805b9fba5b67698058db07905b /test | |
parent | f8e9aed839dce87cebb3e27f20ee8dbe4b782a84 (diff) | |
download | dexon-solidity-7f8ceaadab0c265674b591aa50cfeb8910628b9f.tar dexon-solidity-7f8ceaadab0c265674b591aa50cfeb8910628b9f.tar.gz dexon-solidity-7f8ceaadab0c265674b591aa50cfeb8910628b9f.tar.bz2 dexon-solidity-7f8ceaadab0c265674b591aa50cfeb8910628b9f.tar.lz dexon-solidity-7f8ceaadab0c265674b591aa50cfeb8910628b9f.tar.xz dexon-solidity-7f8ceaadab0c265674b591aa50cfeb8910628b9f.tar.zst dexon-solidity-7f8ceaadab0c265674b591aa50cfeb8910628b9f.zip |
[SMTChecker] Clear state knowledge after external function calls
Diffstat (limited to 'test')
4 files changed, 64 insertions, 1 deletions
diff --git a/test/libsolidity/smtCheckerTests/functions/function_call_does_not_clear_local_vars.sol b/test/libsolidity/smtCheckerTests/functions/function_call_does_not_clear_local_vars.sol index b4260224..0ceb3b46 100644 --- a/test/libsolidity/smtCheckerTests/functions/function_call_does_not_clear_local_vars.sol +++ b/test/libsolidity/smtCheckerTests/functions/function_call_does_not_clear_local_vars.sol @@ -9,5 +9,4 @@ contract C { } } // ---- -// Warning: (99-107): Assertion checker does not yet implement this type of function call. // Warning: (141-144): Assertion checker does not support recursive function calls. diff --git a/test/libsolidity/smtCheckerTests/functions/functions_external_1.sol b/test/libsolidity/smtCheckerTests/functions/functions_external_1.sol new file mode 100644 index 00000000..16482e7a --- /dev/null +++ b/test/libsolidity/smtCheckerTests/functions/functions_external_1.sol @@ -0,0 +1,21 @@ +pragma experimental SMTChecker; + +contract D +{ + function g(uint x) public; +} + +contract C +{ + uint x; + function f(uint y, D d) public { + require(x == y); + assert(x == y); + d.g(y); + // Storage knowledge is cleared after an external call. + assert(x == y); + } +} +// ---- +// Warning: (119-122): Assertion checker does not yet support the type of this variable. +// Warning: (240-254): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/functions/functions_external_2.sol b/test/libsolidity/smtCheckerTests/functions/functions_external_2.sol new file mode 100644 index 00000000..1e704c9d --- /dev/null +++ b/test/libsolidity/smtCheckerTests/functions/functions_external_2.sol @@ -0,0 +1,21 @@ +pragma experimental SMTChecker; + +contract D +{ + function g(uint x) public; +} + +contract C +{ + mapping (uint => uint) map; + function f(uint y, D d) public { + require(map[0] == map[1]); + assert(map[0] == map[1]); + d.g(y); + // Storage knowledge is cleared after an external call. + assert(map[0] == map[1]); + } +} +// ---- +// Warning: (139-142): Assertion checker does not yet support the type of this variable. +// Warning: (280-304): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/functions/functions_external_3.sol b/test/libsolidity/smtCheckerTests/functions/functions_external_3.sol new file mode 100644 index 00000000..dd36ec73 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/functions/functions_external_3.sol @@ -0,0 +1,22 @@ +pragma experimental SMTChecker; + +contract D +{ + function g(uint x) public; +} + +contract C +{ + mapping (uint => uint) storageMap; + function f(uint y, D d) public { + mapping (uint => uint) storage map = storageMap; + require(map[0] == map[1]); + assert(map[0] == map[1]); + d.g(y); + // Storage knowledge is cleared after an external call. + assert(map[0] == map[1]); + } +} +// ---- +// Warning: (146-149): Assertion checker does not yet support the type of this variable. +// Warning: (338-362): Assertion violation happens here |