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

Fix SMT tests

Browse Source
This commit is contained in:
Leonardo Alt 2020-12-10 18:53:25 +01:00
parent ef3bcbda97
commit 64f81fe82b
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);
}
}
// ====
// 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: (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: (435-461): CHC: Assertion violation happens here.
// 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.

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();
}
}
// ====
// 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 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 2529: (121-130): CHC: Empty array "pop" happens here.
// Warning 6328: (230-254): CHC: Assertion violation happens here.