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 #10571 from ethereum/smt_fix_breaking

Browse Source 
Fix SMT tests on breaking
This commit is contained in:
Alex Beregszaszi 2020-12-10 20:05:50 +00:00 committed by GitHub
commit 4b410b8731
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
4 changed files with 10 additions and 6 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_unsafe.sol
View File

@ -37,6 +37,8 @@ contract C {
assert(owner == address(0) || y != z); assert(owner == address(0) || y != z);
} }
} }
// ====
// SMTIgnoreCex: yes
// ---- // ----
// Warning 6328: (435-461): CHC: Assertion violation happens here.\nCounterexample:\nowner = 1, y = 0, z = 0, s = 0\n\n\n\nTransaction trace:\nconstructor()\nState: owner = 0, y = 0, z = 0, s = 0\nf() // Warning 6328: (435-461): CHC: Assertion violation happens here.
// Warning 6328: (594-631): CHC: Assertion violation happens here.\nCounterexample:\nowner = 1, y = 0, z = 0, s = 0\n\n\n\nTransaction trace:\nconstructor()\nState: owner = 1, y = 0, z = 0, s = 0\ninv() // Warning 6328: (594-631): CHC: Assertion violation happens here.

2
test/libsolidity/smtCheckerTests/external_calls/external_inc.sol
View File

@ -18,5 +18,5 @@ contract C {
} }
} }
// ---- // ----
// Warning 6328: (189-203): CHC: Assertion violation happens here.\nCounterexample:\nx = 10, d = 0\n\n\n\nTransaction trace:\nconstructor()\nState: x = 0, d = 0\ninc()\nState: x = 1, d = 0\nf() // Warning 6328: (189-203): CHC: Assertion violation happens here.\nCounterexample:\nx = 10, d = 0\n\n\n\nTransaction trace:\nconstructor()\nState: x = 0, d = 0\ninc()\nState: x = 1, d = 0\ninc()\nState: x = 2, d = 0\nf()
// Warning 2661: (146-149): BMC: Overflow (resulting value larger than 2**256 - 1) happens here. // Warning 2661: (146-149): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.

2
test/libsolidity/smtCheckerTests/types/contract_address_conversion.sol
View File

@ -7,4 +7,4 @@ contract C
} }
} }
// ---- // ----
// Warning 6328: (90-113): CHC: Assertion violation happens here.\nCounterexample:\n\nc = 0\na = 1\n\n\nTransaction trace:\nconstructor()\nf(0, 1) // Warning 6328: (90-113): CHC: Assertion violation happens here.\nCounterexample:\n\nc = 1\na = 0\n\n\nTransaction trace:\nconstructor()\nf(1, 0)

6
test/libsolidity/smtCheckerTests/types/struct/struct_state_var_array_pop_1.sol
View File

@ -20,6 +20,8 @@ contract C {
s.a.pop(); s.a.pop();
} }
} }
// ====
// SMTIgnoreCex: yes
// ---- // ----
// Warning 2529: (121-130): CHC: Empty array "pop" happens here.\nCounterexample:\ns = {x: 0, a: []}\n_x = 0\n\n\nTransaction trace:\nconstructor()\nState: s = {x: 0, a: []}\nf(0) // Warning 2529: (121-130): CHC: Empty array "pop" happens here.
// Warning 6328: (230-254): CHC: Assertion violation happens here.\nCounterexample:\ns = {x: 7720, a: [7720, 0]}\n_x = 7720\n\n\nTransaction trace:\nconstructor()\nState: s = {x: 0, a: []}\nf(7720) // Warning 6328: (230-254): CHC: Assertion violation happens here.