diff options
| author | chriseth <chris@ethereum.org> | 2019-01-22 20:49:41 +0800 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-01-22 20:49:41 +0800 |
| commit | 10d17f245839f208ec5085309022a32cd2502f55 (patch) | |
| tree | b2c9f68980d0d418cd6f511e9f3f3f71369abe25 /test/libsolidity/smtCheckerTests/functions/functions_external_3.sol | |
| parent | 1df8f40cd2fd7b47698d847907b8ca7b47eb488d (diff) | |
| parent | 0ecafe032a84cb6960545dd7f18733430c1f782d (diff) | |
| download | dexon-solidity-10d17f245839f208ec5085309022a32cd2502f55.tar.gz dexon-solidity-10d17f245839f208ec5085309022a32cd2502f55.tar.zst dexon-solidity-10d17f245839f208ec5085309022a32cd2502f55.zip | |
Merge pull request #5836 from ethereum/develop
Merge develop into release for 0.5.3.
Diffstat (limited to 'test/libsolidity/smtCheckerTests/functions/functions_external_3.sol')
| -rw-r--r-- | test/libsolidity/smtCheckerTests/functions/functions_external_3.sol | 22 |
1 files changed, 22 insertions, 0 deletions
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 |