From 0d0add2afcba90dac4ce61e29991bf77a48fc29c Mon Sep 17 00:00:00 2001 From: Leo Alt Date: Thu, 12 May 2022 15:52:29 +0200 Subject: [PATCH] more smtchecker tests --- ..._functions_same_input_over_state_same_output_fail.sol | 4 +++- .../smtCheckerTests/deployment/deploy_trusted_flow.sol | 9 ++++++++- .../deployment/deploy_trusted_state_flow.sol | 4 +++- .../deployment/deploy_trusted_state_flow_3.sol | 4 +--- .../deployment/deploy_trusted_state_flow_4.sol | 2 +- .../call_abstract_constructor_trusted_1.sol | 4 ++-- .../call_abstract_constructor_trusted_2.sol | 3 +-- .../external_calls/call_abstract_trusted_2.sol | 2 -- .../external_calls/call_abstract_trusted_3.sol | 2 -- .../external_calls/external_call_indirect_1.sol | 3 +-- .../external_calls/external_call_indirect_3.sol | 2 +- .../external_calls/external_call_semantic_this_1.sol | 2 +- ...l_state_var_address_inside_array_struct_trusted_2.sol | 2 +- ...nal_call_state_var_address_inside_array_trusted_2.sol | 2 +- ...al_call_state_var_address_inside_struct_trusted_3.sol | 2 +- ..._state_var_contract_inside_array_struct_trusted_1.sol | 2 +- ..._state_var_contract_inside_array_struct_trusted_2.sol | 2 +- ...al_call_state_var_contract_inside_array_trusted_1.sol | 2 +- .../external_calls/external_call_this_with_value_1.sol | 2 +- .../external_hash_known_code_state_trusted.sol | 1 + .../external_calls/external_reentrancy_2.sol | 4 +++- .../functions/getters/external_getter_1.sol | 2 +- .../modifiers/modifier_same_local_variables.sol | 2 +- .../operators/compound_add_array_index.sol | 2 +- .../operators/compound_bitwise_or_int_1.sol | 1 + .../smtCheckerTests/out_of_bounds/array_1.sol | 3 ++- .../smtCheckerTests/special/tx_vars_reentrancy_1.sol | 2 +- .../smtCheckerTests/typecast/string_to_bytes_push_1.sol | 2 +- .../smtCheckerTests/types/fixed_bytes_access_3.sol | 2 -- 29 files changed, 41 insertions(+), 35 deletions(-) diff --git a/test/libsolidity/smtCheckerTests/crypto/crypto_functions_same_input_over_state_same_output_fail.sol b/test/libsolidity/smtCheckerTests/crypto/crypto_functions_same_input_over_state_same_output_fail.sol index b89867c39..fd3b55a8c 100644 --- a/test/libsolidity/smtCheckerTests/crypto/crypto_functions_same_input_over_state_same_output_fail.sol +++ b/test/libsolidity/smtCheckerTests/crypto/crypto_functions_same_input_over_state_same_output_fail.sol @@ -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. diff --git a/test/libsolidity/smtCheckerTests/deployment/deploy_trusted_flow.sol b/test/libsolidity/smtCheckerTests/deployment/deploy_trusted_flow.sol index 5a6720067..f9997c163 100644 --- a/test/libsolidity/smtCheckerTests/deployment/deploy_trusted_flow.sol +++ b/test/libsolidity/smtCheckerTests/deployment/deploy_trusted_flow.sol @@ -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. diff --git a/test/libsolidity/smtCheckerTests/deployment/deploy_trusted_state_flow.sol b/test/libsolidity/smtCheckerTests/deployment/deploy_trusted_state_flow.sol index 94dff06f0..cc54f3a09 100644 --- a/test/libsolidity/smtCheckerTests/deployment/deploy_trusted_state_flow.sol +++ b/test/libsolidity/smtCheckerTests/deployment/deploy_trusted_state_flow.sol @@ -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. diff --git a/test/libsolidity/smtCheckerTests/deployment/deploy_trusted_state_flow_3.sol b/test/libsolidity/smtCheckerTests/deployment/deploy_trusted_state_flow_3.sol index 504362145..260909b87 100644 --- a/test/libsolidity/smtCheckerTests/deployment/deploy_trusted_state_flow_3.sol +++ b/test/libsolidity/smtCheckerTests/deployment/deploy_trusted_state_flow_3.sol @@ -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. diff --git a/test/libsolidity/smtCheckerTests/deployment/deploy_trusted_state_flow_4.sol b/test/libsolidity/smtCheckerTests/deployment/deploy_trusted_state_flow_4.sol index e2036b32f..5bd27c3b8 100644 --- a/test/libsolidity/smtCheckerTests/deployment/deploy_trusted_state_flow_4.sol +++ b/test/libsolidity/smtCheckerTests/deployment/deploy_trusted_state_flow_4.sol @@ -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 diff --git a/test/libsolidity/smtCheckerTests/external_calls/call_abstract_constructor_trusted_1.sol b/test/libsolidity/smtCheckerTests/external_calls/call_abstract_constructor_trusted_1.sol index 3acc9b53b..c066778cb 100644 --- a/test/libsolidity/smtCheckerTests/external_calls/call_abstract_constructor_trusted_1.sol +++ b/test/libsolidity/smtCheckerTests/external_calls/call_abstract_constructor_trusted_1.sol @@ -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() diff --git a/test/libsolidity/smtCheckerTests/external_calls/call_abstract_constructor_trusted_2.sol b/test/libsolidity/smtCheckerTests/external_calls/call_abstract_constructor_trusted_2.sol index 831805ae3..af19ce898 100644 --- a/test/libsolidity/smtCheckerTests/external_calls/call_abstract_constructor_trusted_2.sol +++ b/test/libsolidity/smtCheckerTests/external_calls/call_abstract_constructor_trusted_2.sol @@ -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() diff --git a/test/libsolidity/smtCheckerTests/external_calls/call_abstract_trusted_2.sol b/test/libsolidity/smtCheckerTests/external_calls/call_abstract_trusted_2.sol index 5aeb52284..9c36bfc74 100644 --- a/test/libsolidity/smtCheckerTests/external_calls/call_abstract_trusted_2.sol +++ b/test/libsolidity/smtCheckerTests/external_calls/call_abstract_trusted_2.sol @@ -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!( = 1)\n = 0 -> no errors\n = 1 -> Assertion failed at assert(D(d).x() == 42)\n = 2 -> Assertion failed at assert(D(d).x() == 21)\n = 4 -> Assertion failed at assert(D(d).x() == 21)\n = 5 -> Assertion failed at assert(D(d).x() == 42)\n diff --git a/test/libsolidity/smtCheckerTests/external_calls/call_abstract_trusted_3.sol b/test/libsolidity/smtCheckerTests/external_calls/call_abstract_trusted_3.sol index 785e17aef..317fde003 100644 --- a/test/libsolidity/smtCheckerTests/external_calls/call_abstract_trusted_3.sol +++ b/test/libsolidity/smtCheckerTests/external_calls/call_abstract_trusted_3.sol @@ -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!( = 1)\n((((x' + ((- 1) * x)) = 0) || !(x' <= 665)) && (!(x' >= 667) || ((x' + ((- 1) * x)) = 0)) && !( >= 6))\n = 0 -> no errors\n = 1 -> Assertion failed at assert(D(d).x() == 42)\n = 2 -> Assertion failed at assert(D(d).x() == 21)\n = 4 -> Assertion failed at assert(D(d).x() == 21)\n = 5 -> Assertion failed at assert(D(d).x() == 42)\n = 6 -> Assertion failed at assert(x == 666)\n diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_call_indirect_1.sol b/test/libsolidity/smtCheckerTests/external_calls/external_call_indirect_1.sol index 86d54ae0e..4fef1dc99 100644 --- a/test/libsolidity/smtCheckerTests/external_calls/external_call_indirect_1.sol +++ b/test/libsolidity/smtCheckerTests/external_calls/external_call_indirect_1.sol @@ -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. diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_call_indirect_3.sol b/test/libsolidity/smtCheckerTests/external_calls/external_call_indirect_3.sol index f9a596bc3..2928d20f3 100644 --- a/test/libsolidity/smtCheckerTests/external_calls/external_call_indirect_3.sol +++ b/test/libsolidity/smtCheckerTests/external_calls/external_call_indirect_3.sol @@ -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. diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_call_semantic_this_1.sol b/test/libsolidity/smtCheckerTests/external_calls/external_call_semantic_this_1.sol index 98ffab80f..5e1ad8b1b 100644 --- a/test/libsolidity/smtCheckerTests/external_calls/external_call_semantic_this_1.sol +++ b/test/libsolidity/smtCheckerTests/external_calls/external_call_semantic_this_1.sol @@ -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 diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_address_inside_array_struct_trusted_2.sol b/test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_address_inside_array_struct_trusted_2.sol index e8b9b5880..522c840f5 100644 --- a/test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_address_inside_array_struct_trusted_2.sol +++ b/test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_address_inside_array_struct_trusted_2.sol @@ -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() diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_address_inside_array_trusted_2.sol b/test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_address_inside_array_trusted_2.sol index 5abd44573..f7e31bf74 100644 --- a/test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_address_inside_array_trusted_2.sol +++ b/test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_address_inside_array_trusted_2.sol @@ -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() diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_address_inside_struct_trusted_3.sol b/test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_address_inside_struct_trusted_3.sol index 5563355e3..fff8a9718 100644 --- a/test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_address_inside_struct_trusted_3.sol +++ b/test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_address_inside_struct_trusted_3.sol @@ -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() diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_contract_inside_array_struct_trusted_1.sol b/test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_contract_inside_array_struct_trusted_1.sol index 6471146ee..0b8cd8e59 100644 --- a/test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_contract_inside_array_struct_trusted_1.sol +++ b/test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_contract_inside_array_struct_trusted_1.sol @@ -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. diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_contract_inside_array_struct_trusted_2.sol b/test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_contract_inside_array_struct_trusted_2.sol index c702336a9..97f61fa04 100644 --- a/test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_contract_inside_array_struct_trusted_2.sol +++ b/test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_contract_inside_array_struct_trusted_2.sol @@ -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() diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_contract_inside_array_trusted_1.sol b/test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_contract_inside_array_trusted_1.sol index c3b2f5529..475c39184 100644 --- a/test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_contract_inside_array_trusted_1.sol +++ b/test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_contract_inside_array_trusted_1.sol @@ -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() diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_call_this_with_value_1.sol b/test/libsolidity/smtCheckerTests/external_calls/external_call_this_with_value_1.sol index 06390b12c..c52e0773f 100644 --- a/test/libsolidity/smtCheckerTests/external_calls/external_call_this_with_value_1.sol +++ b/test/libsolidity/smtCheckerTests/external_calls/external_call_this_with_value_1.sol @@ -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 diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_trusted.sol b/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_trusted.sol index 10d9dd709..1c557f7a6 100644 --- a/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_trusted.sol +++ b/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_trusted.sol @@ -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. diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_reentrancy_2.sol b/test/libsolidity/smtCheckerTests/external_calls/external_reentrancy_2.sol index 19ff2bbad..1e8ce8816 100644 --- a/test/libsolidity/smtCheckerTests/external_calls/external_reentrancy_2.sol +++ b/test/libsolidity/smtCheckerTests/external_calls/external_reentrancy_2.sol @@ -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. diff --git a/test/libsolidity/smtCheckerTests/functions/getters/external_getter_1.sol b/test/libsolidity/smtCheckerTests/functions/getters/external_getter_1.sol index 56dc9c3fa..00bfb35ca 100644 --- a/test/libsolidity/smtCheckerTests/functions/getters/external_getter_1.sol +++ b/test/libsolidity/smtCheckerTests/functions/getters/external_getter_1.sol @@ -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. diff --git a/test/libsolidity/smtCheckerTests/modifiers/modifier_same_local_variables.sol b/test/libsolidity/smtCheckerTests/modifiers/modifier_same_local_variables.sol index 89d67b53e..1d86c0fea 100644 --- a/test/libsolidity/smtCheckerTests/modifiers/modifier_same_local_variables.sol +++ b/test/libsolidity/smtCheckerTests/modifiers/modifier_same_local_variables.sol @@ -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) diff --git a/test/libsolidity/smtCheckerTests/operators/compound_add_array_index.sol b/test/libsolidity/smtCheckerTests/operators/compound_add_array_index.sol index 1c6e205d3..4186f39fe 100644 --- a/test/libsolidity/smtCheckerTests/operators/compound_add_array_index.sol +++ b/test/libsolidity/smtCheckerTests/operators/compound_add_array_index.sol @@ -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) diff --git a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_int_1.sol b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_int_1.sol index 252cad51f..fdd8c55cc 100644 --- a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_int_1.sol +++ b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_int_1.sol @@ -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. diff --git a/test/libsolidity/smtCheckerTests/out_of_bounds/array_1.sol b/test/libsolidity/smtCheckerTests/out_of_bounds/array_1.sol index c26e64fcc..ee57f069d 100644 --- a/test/libsolidity/smtCheckerTests/out_of_bounds/array_1.sol +++ b/test/libsolidity/smtCheckerTests/out_of_bounds/array_1.sol @@ -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. diff --git a/test/libsolidity/smtCheckerTests/special/tx_vars_reentrancy_1.sol b/test/libsolidity/smtCheckerTests/special/tx_vars_reentrancy_1.sol index fd2aad6f9..8a31f5b44 100644 --- a/test/libsolidity/smtCheckerTests/special/tx_vars_reentrancy_1.sol +++ b/test/libsolidity/smtCheckerTests/special/tx_vars_reentrancy_1.sol @@ -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. diff --git a/test/libsolidity/smtCheckerTests/typecast/string_to_bytes_push_1.sol b/test/libsolidity/smtCheckerTests/typecast/string_to_bytes_push_1.sol index 4910c417e..33546b49c 100644 --- a/test/libsolidity/smtCheckerTests/typecast/string_to_bytes_push_1.sol +++ b/test/libsolidity/smtCheckerTests/typecast/string_to_bytes_push_1.sol @@ -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() diff --git a/test/libsolidity/smtCheckerTests/types/fixed_bytes_access_3.sol b/test/libsolidity/smtCheckerTests/types/fixed_bytes_access_3.sol index b55293231..b8e1109c9 100644 --- a/test/libsolidity/smtCheckerTests/types/fixed_bytes_access_3.sol +++ b/test/libsolidity/smtCheckerTests/types/fixed_bytes_access_3.sol @@ -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