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

[SMTChecker] updated tests

Browse Source
This commit is contained in:
Martin Blicha 2021-03-02 18:30:17 +01:00
parent 41fc59f00f
commit 9e81c81560
2 changed files with 28 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

14
test/libsolidity/smtCheckerTests/typecast/string_to_bytes_push_1.sol Normal file
View File

@ -0,0 +1,14 @@
pragma experimental SMTChecker;
contract C {
string x;
function s() public {
x = "abc";
bytes(x).push("a");
assert(bytes(x).length == 4); // should hold
assert(bytes(x).length == 3); // should fail
}
}
// ----
// Warning 6328: (165-193): CHC: Assertion violation happens here.\nCounterexample:\nx = [97, 98, 99, 97]\n\nTransaction trace:\nC.constructor()\nState: x = []\nC.s()

14
test/libsolidity/smtCheckerTests/typecast/string_to_bytes_push_2.sol Normal file
View File

@ -0,0 +1,14 @@
pragma experimental SMTChecker;
contract C {
string x;
function s() public {
x = "abc";
((bytes(((x))))).push("a");
assert(bytes(x).length == 4); // should hold
assert(bytes(x).length == 3); // should fail
}
}
// ----
// Warning 6328: (173-201): CHC: Assertion violation happens here.\nCounterexample:\nx = [97, 98, 99, 97]\n\nTransaction trace:\nC.constructor()\nState: x = []\nC.s()