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 #9052 from ethereum/smt_add_test_delete_m_d_array

Browse Source 
[SMTChecker] Add test that deletes arrays
This commit is contained in:
Leonardo 2020-05-28 16:14:55 +02:00 committed by GitHub
commit 1051cea91c
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
1 changed files with 42 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

42
test/libsolidity/smtCheckerTests/operators/delete_multid_array.sol Normal file
View File

@ -0,0 +1,42 @@
pragma experimental SMTChecker;
contract C {
uint[] a;
uint[][] b;
function f(uint x, uint y, uint v) public {
a[x] = v;
delete a;
assert(a[y] == 0);
}
function g(uint x, uint y, uint v) public {
b[x][y] = v;
delete b;
assert(b[y][x] == 0);
}
function h(uint x, uint y, uint v) public {
b[x][y] = v;
delete b[x];
// Not necessarily the case.
assert(b[y][x] == 0);
}
function i(uint x, uint y, uint v) public {
b[x][y] = v;
delete b[y];
assert(b[y][x] == 0);
}
function j(uint x, uint y, uint z, uint v) public {
b[x][y] = v;
delete b[z];
// Not necessarily the case.
assert(b[y][x] == 0);
}
function setA(uint x, uint y) public {
a[x] = y;
}
function setB(uint x, uint y, uint z) public {
b[x][y] = z;
}
}
// ----
// Warning: (372-392): Assertion violation happens here
// Warning: (617-637): Assertion violation happens here