cerc-io/solidity
11
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

more smtchecker tests

Browse Source
This commit is contained in:
Leo Alt 2022-05-12 15:52:29 +02:00
parent 98930344e8
commit 0d0add2afc
29 changed files with 41 additions and 35 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
test/libsolidity/smtCheckerTests/crypto/crypto_functions_same_input_over_state_same_output_fail.sol
View File

@ -48,10 +48,12 @@ contract C {
// Warning 1218: (693-712): CHC: Error trying to invoke SMT solver.
// Warning 1218: (716-735): CHC: Error trying to invoke SMT solver.
// Warning 1218: (739-758): CHC: Error trying to invoke SMT solver.
// Warning 1218: (762-781): CHC: Error trying to invoke SMT solver.
// Warning 6328: (693-712): CHC: Assertion violation might happen here.
// Warning 6328: (716-735): CHC: Assertion violation might happen here.
// Warning 6328: (739-758): CHC: Assertion violation might happen here.
// Warning 6328: (762-781): CHC: Assertion violation happens here.
// Warning 6328: (762-781): CHC: Assertion violation might happen here.
// Warning 4661: (693-712): BMC: Assertion violation happens here.
// Warning 4661: (716-735): BMC: Assertion violation happens here.
// Warning 4661: (739-758): BMC: Assertion violation happens here.
// Warning 4661: (762-781): BMC: Assertion violation happens here.

9
test/libsolidity/smtCheckerTests/deployment/deploy_trusted_flow.sol
View File

@ -20,5 +20,12 @@ contract C {
// SMTExtCalls: trusted
// ----
// Warning 4984: (47-50): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
// Warning 6328: (304-322): CHC: Assertion violation happens here.
// Warning 6328: (167-185): CHC: Assertion violation might happen here.
// Warning 6328: (215-233): CHC: Assertion violation might happen here.
// Warning 6328: (267-285): CHC: Assertion violation might happen here.
// Warning 6328: (304-322): CHC: Assertion violation might happen here.
// Warning 2661: (47-50): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 4661: (167-185): BMC: Assertion violation happens here.
// Warning 4661: (215-233): BMC: Assertion violation happens here.
// Warning 4661: (267-285): BMC: Assertion violation happens here.
// Warning 4661: (304-322): BMC: Assertion violation happens here.

4
test/libsolidity/smtCheckerTests/deployment/deploy_trusted_state_flow.sol
View File

@ -18,6 +18,8 @@ contract C {
// SMTEngine: all
// SMTExtCalls: trusted
// ----
// Warning 1218: (233-251): CHC: Error trying to invoke SMT solver.
// Warning 4984: (47-50): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
// Warning 6328: (233-251): CHC: Assertion violation happens here.
// Warning 6328: (233-251): CHC: Assertion violation might happen here.
// Warning 2661: (47-50): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 4661: (233-251): BMC: Assertion violation happens here.

4
test/libsolidity/smtCheckerTests/deployment/deploy_trusted_state_flow_3.sol
View File

@ -18,6 +18,4 @@ contract C {
// SMTEngine: all
// SMTExtCalls: trusted
// ----
// Warning 1218: (204-222): CHC: Error trying to invoke SMT solver.
// Warning 6328: (204-222): CHC: Assertion violation might happen here.
// Warning 4661: (204-222): BMC: Assertion violation happens here.
// Warning 6328: (204-222): CHC: Assertion violation happens here.

2
test/libsolidity/smtCheckerTests/deployment/deploy_trusted_state_flow_4.sol
View File

@ -17,4 +17,4 @@ contract C {
// SMTEngine: all
// SMTExtCalls: trusted
// ----
// Warning 6328: (199-212): CHC: Assertion violation happens here.\nCounterexample:\nd = 0\n\nTransaction trace:\nC.constructor()\nState: d = 0\nC.g()\n D.f() -- trusted external call
// Warning 6328: (199-212): CHC: Assertion violation happens here.\nCounterexample:\nd = (- 1)\n\nTransaction trace:\nC.constructor()\nState: d = (- 1)\nC.g()\n D.f() -- trusted external call

4
test/libsolidity/smtCheckerTests/external_calls/call_abstract_constructor_trusted_1.sol
View File

@ -23,5 +23,5 @@ contract C {
// SMTExtCalls: trusted
// ----
// Warning 6328: (231-253): CHC: Assertion violation happens here.\nCounterexample:\n\nd = 0x0119\ny = 0\n\nTransaction trace:\nC.constructor()
// Warning 6328: (293-307): CHC: Assertion violation happens here.\nCounterexample:\n\nd = 0x188b\ny = 0\n\nTransaction trace:\nC.constructor()
// Warning 6328: (359-374): CHC: Assertion violation happens here.\nCounterexample:\n\nd = 0x0217\ny = 0\n\nTransaction trace:\nC.constructor()
// Warning 6328: (293-307): CHC: Assertion violation happens here.\nCounterexample:\n\nd = 0x0217\ny = 3\n\nTransaction trace:\nC.constructor()
// Warning 6328: (359-374): CHC: Assertion violation happens here.\nCounterexample:\n\nd = 0x188b\ny = 0\n\nTransaction trace:\nC.constructor()

3
test/libsolidity/smtCheckerTests/external_calls/call_abstract_constructor_trusted_2.sol
View File

@ -19,7 +19,6 @@ contract C {
// SMTExtCalls: trusted
// ----
// Warning 9302: (257-293): Return value of low-level calls not used.
// Warning 6031: (279-285): Internal error: Expression undefined for SMT solver.
// Warning 6328: (216-238): CHC: Assertion violation happens here.\nCounterexample:\n\nd = 0x0119\n\nTransaction trace:\nC.constructor()
// Warning 6328: (297-319): CHC: Assertion violation happens here.\nCounterexample:\n\nd = 0x1720\n\nTransaction trace:\nC.constructor()
// Warning 6328: (404-426): CHC: Assertion violation happens here.\nCounterexample:\n\nd = 0x0217\n\nTransaction trace:\nC.constructor()
// Warning 6328: (404-426): CHC: Assertion violation happens here.\nCounterexample:\n\nd = 0x1720\n\nTransaction trace:\nC.constructor()

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

@ -20,8 +20,6 @@ contract C {
// SMTIgnoreCex: yes
// ----
// Warning 9302: (263-299): Return value of low-level calls not used.
// Warning 6031: (285-291): Internal error: Expression undefined for SMT solver.
// Warning 6328: (222-244): CHC: Assertion violation happens here.
// Warning 6328: (303-325): CHC: Assertion violation happens here.
// Warning 6328: (410-432): CHC: Assertion violation happens here.
// Info 1180: Reentrancy property(ies) for :C:\n!(<errorCode> = 1)\n<errorCode> = 0 -> no errors\n<errorCode> = 1 -> Assertion failed at assert(D(d).x() == 42)\n<errorCode> = 2 -> Assertion failed at assert(D(d).x() == 21)\n<errorCode> = 4 -> Assertion failed at assert(D(d).x() == 21)\n<errorCode> = 5 -> Assertion failed at assert(D(d).x() == 42)\n

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

@ -24,8 +24,6 @@ contract C {
// SMTIgnoreCex: yes
// ----
// Warning 9302: (284-320): Return value of low-level calls not used.
// Warning 6031: (306-312): Internal error: Expression undefined for SMT solver.
// Warning 6328: (243-265): CHC: Assertion violation happens here.
// Warning 6328: (324-346): CHC: Assertion violation happens here.
// Warning 6328: (431-453): CHC: Assertion violation happens here.
// Info 1180: Reentrancy property(ies) for :C:\n!(<errorCode> = 1)\n((((x' + ((- 1) * x)) = 0) || !(x' <= 665)) && (!(x' >= 667) || ((x' + ((- 1) * x)) = 0)) && !(<errorCode> >= 6))\n<errorCode> = 0 -> no errors\n<errorCode> = 1 -> Assertion failed at assert(D(d).x() == 42)\n<errorCode> = 2 -> Assertion failed at assert(D(d).x() == 21)\n<errorCode> = 4 -> Assertion failed at assert(D(d).x() == 21)\n<errorCode> = 5 -> Assertion failed at assert(D(d).x() == 42)\n<errorCode> = 6 -> Assertion failed at assert(x == 666)\n

3
test/libsolidity/smtCheckerTests/external_calls/external_call_indirect_1.sol
View File

@ -36,6 +36,5 @@ contract C {
// SMTEngine: chc
// SMTExtCalls: trusted
// ----
// Warning 1218: (256-277): CHC: Error trying to invoke SMT solver.
// Warning 6328: (256-277): CHC: Assertion violation might happen here.
// Warning 6328: (256-277): CHC: Assertion violation happens here.
// Warning 6328: (533-554): CHC: Assertion violation might happen here.

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

@ -41,4 +41,4 @@ contract C {
// SMTEngine: chc
// SMTExtCalls: trusted
// ----
// Warning 6328: (561-582): CHC: Assertion violation happens here.
// Warning 6328: (561-582): CHC: Assertion violation might happen here.

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

@ -13,4 +13,4 @@ contract C {
// SMTExtCalls: trusted
// SMTTargets: assert
// ----
// Warning 6328: (147-161): CHC: Assertion violation happens here.
// Warning 6328: (147-161): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.f()\n C.i() -- trusted external call

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

@ -21,4 +21,4 @@ contract C {
// SMTExtCalls: trusted
// SMTTargets: assert
// ----
// Warning 6328: (253-280): CHC: Assertion violation happens here.
// Warning 6328: (253-280): CHC: Assertion violation happens here.\nCounterexample:\nss = [{d: 0x4706}]\n\nTransaction trace:\nC.constructor()\nState: ss = [{d: 0x4706}]\nC.f()

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

@ -17,4 +17,4 @@ contract C {
// SMTExtCalls: trusted
// SMTTargets: assert
// ----
// Warning 6328: (183-208): CHC: Assertion violation happens here.\nCounterexample:\nds = [0x0]\n\nTransaction trace:\nC.constructor()\nState: ds = [0x0]\nC.f()
// Warning 6328: (183-208): CHC: Assertion violation happens here.\nCounterexample:\nds = [0x25]\n\nTransaction trace:\nC.constructor()\nState: ds = [0x25]\nC.f()

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

@ -23,4 +23,4 @@ contract C {
// SMTExtCalls: trusted
// SMTTargets: assert
// ----
// Warning 6328: (223-248): CHC: Assertion violation happens here.
// Warning 6328: (223-248): CHC: Assertion violation happens here.\nCounterexample:\nt = {s: {d: 0x5039}}\n\nTransaction trace:\nC.constructor()\nState: t = {s: {d: 0x5039}}\nC.f()

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

@ -20,4 +20,4 @@ contract C {
// SMTExtCalls: trusted
// SMTTargets: assert
// ----
// Warning 6328: (192-216): CHC: Assertion violation happens here.\nCounterexample:\nss = [{d: 3}]\n\nTransaction trace:\nC.constructor()\nState: ss = [{d: 3}]\nC.f()
// Warning 6328: (192-216): CHC: Assertion violation happens here.

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

@ -21,4 +21,4 @@ contract C {
// SMTExtCalls: trusted
// SMTTargets: assert
// ----
// Warning 6328: (235-259): CHC: Assertion violation happens here.\nCounterexample:\nss = [{d: 3}]\n\nTransaction trace:\nC.constructor()\nState: ss = [{d: 3}]\nC.f()
// Warning 6328: (235-259): CHC: Assertion violation happens here.\nCounterexample:\nss = [{d: 20819}]\n\nTransaction trace:\nC.constructor()\nState: ss = [{d: 20819}]\nC.f()

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

@ -18,4 +18,4 @@ contract C {
// SMTExtCalls: trusted
// SMTTargets: assert
// ----
// Warning 6328: (208-230): CHC: Assertion violation happens here.\nCounterexample:\nds = [37]\n\nTransaction trace:\nC.constructor()\nState: ds = [37]\nC.f()
// Warning 6328: (208-230): CHC: Assertion violation happens here.\nCounterexample:\nds = [39]\n\nTransaction trace:\nC.constructor()\nState: ds = [39]\nC.f()

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

@ -11,4 +11,4 @@ contract C {
// ====
// SMTEngine: all
// ----
// Warning 6328: (157-192): CHC: Assertion violation happens here.
// Warning 6328: (157-192): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.g()\n C.h() -- trusted external call

1
test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_trusted.sol
View File

@ -32,4 +32,5 @@ contract C {
// SMTEngine: chc
// SMTExtCalls: trusted
// ----
// Warning 6328: (355-381): CHC: Assertion violation might happen here.
// Warning 6328: (385-399): CHC: Assertion violation might happen here.

4
test/libsolidity/smtCheckerTests/external_calls/external_reentrancy_2.sol
View File

@ -13,4 +13,6 @@ contract C {
// ====
// SMTEngine: all
// ----
// Warning 6328: (117-131): CHC: Assertion violation happens here.\nCounterexample:\nlocked = false\ntarget = 0x0\n\nTransaction trace:\nC.constructor()\nState: locked = true\nC.call(0x0)\n D(target).e() -- untrusted external call, synthesized as:\n C.call(0x0) -- reentrant call
// Warning 1218: (117-131): CHC: Error trying to invoke SMT solver.
// Warning 6328: (117-131): CHC: Assertion violation might happen here.
// Warning 4661: (117-131): BMC: Assertion violation happens here.

2
test/libsolidity/smtCheckerTests/functions/getters/external_getter_1.sol
View File

@ -19,4 +19,4 @@ contract C {
// SMTExtCalls: trusted
// SMTTargets: assert
// ----
// Warning 6328: (203-221): CHC: Assertion violation happens here.\nCounterexample:\n\na = 42\n\nTransaction trace:\nC.constructor()\nC.f()\n D.g() -- trusted external call
// Warning 6328: (203-221): CHC: Assertion violation happens here.

2
test/libsolidity/smtCheckerTests/modifiers/modifier_same_local_variables.sol
View File

@ -12,4 +12,4 @@ contract C
// ====
// SMTEngine: all
// ----
// Warning 6328: (88-102): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 3\nx = 2\n\nTransaction trace:\nC.constructor()\nC.f(3)
// Warning 6328: (88-102): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 0\nx = 2\n\nTransaction trace:\nC.constructor()\nC.f(0)

2
test/libsolidity/smtCheckerTests/operators/compound_add_array_index.sol
View File

@ -20,4 +20,4 @@ contract C
// SMTEngine: all
// SMTIgnoreOS: macos
// ----
// Warning 6328: (262-284): CHC: Assertion violation happens here.\nCounterexample:\narray = [299, 0]\nx = 99\np = 0\n\nTransaction trace:\nC.constructor()\nState: array = [0, 0]\nC.f(99, 0)
// Warning 6328: (262-284): CHC: Assertion violation happens here.\nCounterexample:\narray = [200, 0]\nx = 0\np = 0\n\nTransaction trace:\nC.constructor()\nState: array = [0, 0]\nC.f(0, 0)

1
test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_int_1.sol
View File

@ -12,6 +12,7 @@ contract C {
// SMTIgnoreOS: macos
// ----
// Warning 6368: (76-81): CHC: Out of bounds access might happen here.
// Warning 6368: (76-84): CHC: Out of bounds access might happen here.
// Warning 6368: (119-124): CHC: Out of bounds access might happen here.
// Warning 6368: (119-127): CHC: Out of bounds access might happen here.
// Warning 6368: (149-154): CHC: Out of bounds access might happen here.

3
test/libsolidity/smtCheckerTests/out_of_bounds/array_1.sol
View File

@ -21,6 +21,7 @@ contract C {
// SMTIgnoreOS: macos
// ----
// Warning 4984: (112-115): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
// Warning 3944: (181-184): CHC: Underflow (resulting value less than 0) might happen here.
// Warning 6368: (259-263): CHC: Out of bounds access happens here.\nCounterexample:\na = [0], l = 1\n = 0\n\nTransaction trace:\nC.constructor()\nState: a = [], l = 0\nC.p()\nState: a = [0], l = 1\nC.r()
// Info 1180: Contract invariant(s) for :C:\n((a.length + ((- 1) * l)) <= 0)\n
// Warning 2661: (112-115): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 4144: (181-184): BMC: Underflow (resulting value less than 0) happens here.

2
test/libsolidity/smtCheckerTests/special/tx_vars_reentrancy_1.sol
View File

@ -14,4 +14,4 @@ contract C {
// SMTIgnoreCex: yes
// SMTIgnoreOS: macos
// ----
// Warning 6328: (135-169): CHC: Assertion violation happens here.\nCounterexample:\n\n_i = 0\nx = 9726\n\nTransaction trace:\nC.constructor()\nC.g(0){ msg.value: 2070 }\n _i.f() -- untrusted external call, synthesized as:\n C.g(0){ msg.value: 0 } -- reentrant call\n _i.f() -- untrusted external call
// Warning 6328: (135-169): CHC: Assertion violation happens here.

2
test/libsolidity/smtCheckerTests/typecast/string_to_bytes_push_1.sol
View File

@ -11,4 +11,4 @@ contract C {
// ====
// SMTEngine: all
// ----
// Warning 6328: (132-160): CHC: Assertion violation happens here.\nCounterexample:\nx = [0x61, 0x62, 0x63, 0x61]\n\nTransaction trace:\nC.constructor()\nState: x = []\nC.s()
// Warning 6328: (132-160): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nState: x = []\nC.s()

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

@ -32,6 +32,4 @@ contract C {
// SMTEngine: all
// SMTIgnoreOS: macos
// ----
// Warning 6368: (374-381): CHC: Out of bounds access might happen here.
// Warning 6368: (456-462): CHC: Out of bounds access happens here.
// Info 1180: Contract invariant(s) for :C:\n!(a.length <= 4)\n