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 #10621 from ethereum/smt_fix_breaking_again

Browse Source 
SMTChecker fix breaking again
This commit is contained in:
Alex Beregszaszi 2020-12-15 20:30:37 +00:00 committed by GitHub
commit b764e06c76
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
2 changed files with 7 additions and 7 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
test/libsolidity/smtCheckerTests/array_members/push_as_lhs_and_rhs_bytes.sol
View File

@ -9,8 +9,8 @@ contract C {
assert(b[length - 1] == 0); assert(b[length - 1] == 0);
assert(b[length - 1] == b[length - 2]); assert(b[length - 1] == b[length - 2]);
// Fails // Fails
assert(b[length - 1] == byte(uint8(1))); assert(b[length - 1] == bytes1(uint8(1)));
} }
} }
// ---- // ----
// Warning 6328: (236-275): CHC: Assertion violation happens here.\nCounterexample:\nb = [0, 0]\n\n\n\nTransaction trace:\nconstructor()\nState: b = []\nf() // Warning 6328: (236-277): CHC: Assertion violation happens here.\nCounterexample:\nb = [0, 0]\n\n\n\nTransaction trace:\nconstructor()\nState: b = []\nf()

10
test/libsolidity/smtCheckerTests/array_members/push_as_lhs_bytes.sol
View File

@ -5,18 +5,18 @@ contract C {
function f() public { function f() public {
require(b.length == 0); require(b.length == 0);
b.push() = byte(uint8(1)); b.push() = bytes1(uint8(1));
assert(b[0] == byte(uint8(1))); assert(b[0] == bytes1(uint8(1)));
} }
function g() public { function g() public {
byte one = byte(uint8(1)); bytes1 one = bytes1(uint8(1));
b.push() = one; b.push() = one;
assert(b[b.length - 1] == one); assert(b[b.length - 1] == one);
// Fails // Fails
assert(b[b.length - 1] == byte(uint8(100))); assert(b[b.length - 1] == bytes1(uint8(100)));
} }
} }
// ---- // ----
// Warning 6328: (290-333): CHC: Assertion violation happens here.\nCounterexample:\nb = [1]\n\n\n\nTransaction trace:\nconstructor()\nState: b = []\ng() // Warning 6328: (298-343): CHC: Assertion violation happens here.\nCounterexample:\nb = [1]\n\n\n\nTransaction trace:\nconstructor()\nState: b = []\ng()