From 9f171c0f06975a6852c8afac8361bb5a976c8d51 Mon Sep 17 00:00:00 2001 From: Leo Alt Date: Wed, 12 Jan 2022 14:46:30 +0100 Subject: [PATCH] update smtchecker tests for new z3 --- .circleci/config.yml | 16 ++++++++-------- .circleci/osx_install_dependencies.sh | 2 +- CMakeLists.txt | 2 +- scripts/build_emscripten.sh | 4 ++-- .../blockchain_state/balance_receive_2.sol | 2 +- .../balance_receive_ext_calls_2.sol | 2 +- .../branches_in_modifiers_2.sol | 2 +- .../external_calls/call_with_value_1.sol | 2 +- .../external_call_from_constructor_3.sol | 2 +- .../external_call_with_value_2.sol | 2 +- .../external_hash_known_code_state.sol | 2 +- ...hash_known_code_state_reentrancy_indirect.sol | 4 +++- .../external_calls/external_reentrancy_2.sol | 4 +++- .../functions/functions_external_2.sol | 2 +- .../virtual_function_called_by_constructor.sol | 2 +- .../assignment_contract_member_variable.sol | 2 +- .../operators/compound_add_array_index.sol | 2 +- .../operators/conditional_assignment_6.sol | 2 +- .../special/tx_vars_reentrancy_1.sol | 2 +- .../special/tx_vars_reentrancy_2.sol | 4 +++- .../try_catch/try_public_var_mapping.sol | 2 +- .../types/address_transfer_insufficient.sol | 2 +- .../types/mapping_equal_keys_2.sol | 2 +- .../types/static_array_length_1.sol | 2 +- .../struct_aliasing_parameter_storage_2.sol | 2 +- .../struct_aliasing_parameter_storage_3.sol | 2 +- .../smtCheckerTests/userTypes/fixedpoint.sol | 2 +- 27 files changed, 41 insertions(+), 35 deletions(-) diff --git a/.circleci/config.yml b/.circleci/config.yml index 1b1fbbdb0..56a4af30a 100644 --- a/.circleci/config.yml +++ b/.circleci/config.yml @@ -9,20 +9,20 @@ version: 2.1 parameters: ubuntu-2004-docker-image: type: string - # solbuildpackpusher/solidity-buildpack-deps:ubuntu2004-9 - default: "solbuildpackpusher/solidity-buildpack-deps@sha256:3d8a912e8e78e98cd217955d06d98608ad60adc67728d4c3a569991235fa1abb" + # solbuildpackpusher/solidity-buildpack-deps:ubuntu2004-10 + default: "solbuildpackpusher/solidity-buildpack-deps@sha256:e61939751ff9777307857361f712b581bfc8a8aaae75fab7b50febc764710587" ubuntu-2004-clang-docker-image: type: string - # solbuildpackpusher/solidity-buildpack-deps:ubuntu2004.clang-9 - default: "solbuildpackpusher/solidity-buildpack-deps@sha256:a1ba002cae17279d1396a898b04e4e9c45602ad881295db3e2f484a7e24f6f43" + # solbuildpackpusher/solidity-buildpack-deps:ubuntu2004.clang-10 + default: "solbuildpackpusher/solidity-buildpack-deps@sha256:0de8c68f084120b2a165406e3a0c2aab58b32f5b7182c2322245245f1d243b8d" ubuntu-1604-clang-ossfuzz-docker-image: type: string - # solbuildpackpusher/solidity-buildpack-deps:ubuntu1604.clang.ossfuzz-14 - default: "solbuildpackpusher/solidity-buildpack-deps@sha256:f353823cce2f6cd2f9f1459d86cd76fdfc551a0261d87626615ea6c1d8f90587" + # solbuildpackpusher/solidity-buildpack-deps:ubuntu1604.clang.ossfuzz-15 + default: "solbuildpackpusher/solidity-buildpack-deps@sha256:87f1a57586eec194a6217ab624efc69d3d9af2f7ac8ca36497ad57488c2f08ae" emscripten-docker-image: type: string - # solbuildpackpusher/solidity-buildpack-deps:emscripten-8 - default: "solbuildpackpusher/solidity-buildpack-deps@sha256:842d6074e0e7e5355c89122c1cafc1fdb59696596750e7d56e5f35c0d883ad59" + # solbuildpackpusher/solidity-buildpack-deps:emscripten-9 + default: "solbuildpackpusher/solidity-buildpack-deps@sha256:d51534dfdd05ece86f69ed7beafd68c15b88606da00a4b7fe2873ccfbd0dce24" evm-version: type: string default: london diff --git a/.circleci/osx_install_dependencies.sh b/.circleci/osx_install_dependencies.sh index 36d336774..9e8d14963 100755 --- a/.circleci/osx_install_dependencies.sh +++ b/.circleci/osx_install_dependencies.sh @@ -61,7 +61,7 @@ then ./scripts/install_obsolete_jsoncpp_1_7_4.sh # z3 - z3_version="4.8.13" + z3_version="4.8.14" z3_dir="z3-${z3_version}-x64-osx-10.16" z3_package="${z3_dir}.zip" wget "https://github.com/Z3Prover/z3/releases/download/z3-${z3_version}/${z3_package}" diff --git a/CMakeLists.txt b/CMakeLists.txt index f3a03d94e..99d765980 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -65,7 +65,7 @@ configure_file("${CMAKE_SOURCE_DIR}/cmake/templates/license.h.in" include/licens include(EthOptions) configure_project(TESTS) -set(LATEST_Z3_VERSION "4.8.13") +set(LATEST_Z3_VERSION "4.8.14") set(MINIMUM_Z3_VERSION "4.8.0") find_package(Z3) if (${Z3_FOUND}) diff --git a/scripts/build_emscripten.sh b/scripts/build_emscripten.sh index f6c9151eb..16e9078f3 100755 --- a/scripts/build_emscripten.sh +++ b/scripts/build_emscripten.sh @@ -34,7 +34,7 @@ else BUILD_DIR="$1" fi -# solbuildpackpusher/solidity-buildpack-deps:emscripten-8 +# solbuildpackpusher/solidity-buildpack-deps:emscripten-9 docker run -v "$(pwd):/root/project" -w /root/project \ - solbuildpackpusher/solidity-buildpack-deps@sha256:842d6074e0e7e5355c89122c1cafc1fdb59696596750e7d56e5f35c0d883ad59 \ + solbuildpackpusher/solidity-buildpack-deps@sha256:d51534dfdd05ece86f69ed7beafd68c15b88606da00a4b7fe2873ccfbd0dce24\ ./scripts/ci/build_emscripten.sh "$BUILD_DIR" diff --git a/test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_2.sol b/test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_2.sol index c4714e2e3..bbf91ade4 100644 --- a/test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_2.sol +++ b/test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_2.sol @@ -16,5 +16,5 @@ contract C { // SMTEngine: all // ---- // Warning 4984: (266-272): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\nx = 115792089237316195423570985008687907853269984665640564039457584007913129639926, once = true\n\nTransaction trace:\nC.constructor(){ msg.value: 28100 }\nState: x = 115792089237316195423570985008687907853269984665640564039457584007913129639926, once = false\nC.f(){ msg.value: 8 } -// Warning 6328: (235-273): CHC: Assertion violation happens here.\nCounterexample:\nx = 0, once = true\n\nTransaction trace:\nC.constructor(){ msg.value: 0 }\nState: x = 0, once = false\nC.f(){ msg.value: 8 } +// Warning 6328: (235-273): CHC: Assertion violation happens here.\nCounterexample:\nx = 0, once = true\n\nTransaction trace:\nC.constructor(){ msg.value: 0 }\nState: x = 0, once = false\nC.f(){ msg.value: 2 } // Info 1180: Contract invariant(s) for :C:\nonce\n diff --git a/test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_ext_calls_2.sol b/test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_ext_calls_2.sol index c53f156d6..28c4734bd 100644 --- a/test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_ext_calls_2.sol +++ b/test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_ext_calls_2.sol @@ -12,4 +12,4 @@ contract C { // ---- // Warning 9302: (82-93): Return value of low-level calls not used. // Warning 6328: (97-131): CHC: Assertion violation happens here. -// Info 1180: Reentrancy property(ies) for :C:\n(!( >= 2) && (((:var 1).balances[address(this)] + ((- 1) * (:var 0).balances[address(this)])) <= 0))\n = 0 -> no errors\n = 1 -> Assertion failed at assert(address(this).balance == x)\n = 2 -> Assertion failed at assert(address(this).balance >= x)\n +// Info 1180: Reentrancy property(ies) for :C:\n((((:var 1).balances[address(this)] + ((- 1) * (:var 0).balances[address(this)])) <= 0) && !( >= 2))\n = 0 -> no errors\n = 1 -> Assertion failed at assert(address(this).balance == x)\n = 2 -> Assertion failed at assert(address(this).balance >= x)\n diff --git a/test/libsolidity/smtCheckerTests/control_flow/branches_with_return/branches_in_modifiers_2.sol b/test/libsolidity/smtCheckerTests/control_flow/branches_with_return/branches_in_modifiers_2.sol index f08a26bf7..98b551c17 100644 --- a/test/libsolidity/smtCheckerTests/control_flow/branches_with_return/branches_in_modifiers_2.sol +++ b/test/libsolidity/smtCheckerTests/control_flow/branches_with_return/branches_in_modifiers_2.sol @@ -45,5 +45,5 @@ contract C { // SMTIgnoreOS: macos // ---- // Warning 6328: (255-269): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.test()\n C.reset_if_overflow() -- internal call -// Warning 6328: (502-519): CHC: Assertion violation happens here.\nCounterexample:\nx = 2\noldx = 1\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.set(1)\nState: x = 1\nC.test()\n C.reset_if_overflow() -- internal call +// Warning 6328: (502-519): CHC: Assertion violation happens here. // Warning 6328: (615-629): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.set(10)\nState: x = 10\nC.test()\n C.reset_if_overflow() -- internal call diff --git a/test/libsolidity/smtCheckerTests/external_calls/call_with_value_1.sol b/test/libsolidity/smtCheckerTests/external_calls/call_with_value_1.sol index f9293f693..813185adf 100644 --- a/test/libsolidity/smtCheckerTests/external_calls/call_with_value_1.sol +++ b/test/libsolidity/smtCheckerTests/external_calls/call_with_value_1.sol @@ -12,5 +12,5 @@ contract C { // ---- // Warning 9302: (96-117): Return value of low-level calls not used. // Warning 6328: (121-156): CHC: Assertion violation might happen here. -// Warning 6328: (175-211): CHC: Assertion violation happens here.\nCounterexample:\n\ni = 0x0\n\nTransaction trace:\nC.constructor()\nC.g(0x0)\n i.call{value: 10}("") -- untrusted external call +// Warning 6328: (175-211): CHC: Assertion violation happens here. // Warning 4661: (121-156): BMC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_call_from_constructor_3.sol b/test/libsolidity/smtCheckerTests/external_calls/external_call_from_constructor_3.sol index 9d27d6d3b..eb5cd97dd 100644 --- a/test/libsolidity/smtCheckerTests/external_calls/external_call_from_constructor_3.sol +++ b/test/libsolidity/smtCheckerTests/external_calls/external_call_from_constructor_3.sol @@ -20,4 +20,4 @@ contract C { // SMTEngine: all // ---- // Warning 6328: (69-85): CHC: Assertion violation happens here.\nCounterexample:\n\n_x = 100\n = 0\n\nTransaction trace:\nState.constructor()\nState.f(100) -// Warning 6328: (203-217): CHC: Assertion violation happens here.\nCounterexample:\ns = 0, z = 0\n\nTransaction trace:\nC.constructor()\nState: s = 0, z = 0\nC.f() +// Warning 6328: (203-217): CHC: Assertion violation happens here.\nCounterexample:\ns = 0, z = 3\n\nTransaction trace:\nC.constructor()\nState: s = 0, z = 3\nC.f() diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_call_with_value_2.sol b/test/libsolidity/smtCheckerTests/external_calls/external_call_with_value_2.sol index f6c833858..4b51d9d9e 100644 --- a/test/libsolidity/smtCheckerTests/external_calls/external_call_with_value_2.sol +++ b/test/libsolidity/smtCheckerTests/external_calls/external_call_with_value_2.sol @@ -14,5 +14,5 @@ contract C { // SMTEngine: all // ---- // Warning 6328: (150-186): CHC: Assertion violation might happen here. -// Warning 6328: (205-240): CHC: Assertion violation happens here.\nCounterexample:\n\ni = 0\n\nTransaction trace:\nC.constructor()\nC.g(0)\n i.f{value: 0}() -- untrusted external call +// Warning 6328: (205-240): CHC: Assertion violation happens here. // Warning 4661: (150-186): BMC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state.sol b/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state.sol index 2468a1a72..317400e1d 100644 --- a/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state.sol +++ b/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state.sol @@ -36,4 +36,4 @@ contract C { // SMTIgnoreCex: yes // ---- // Warning 6328: (495-532): CHC: Assertion violation happens here. -// Info 1180: Reentrancy property(ies) for :C:\n(((owner + ((- 1) * owner')) <= 0) && !( = 1) && ((owner + ((- 1) * owner')) >= 0))\n = 0 -> no errors\n = 1 -> Assertion failed at assert(prevOwner == owner)\n = 3 -> Assertion failed at assert(owner == address(0) || y != z)\n +// Info 1180: Reentrancy property(ies) for :C:\n(((owner + ((- 1) * owner')) >= 0) && !( = 1) && ((owner + ((- 1) * owner')) <= 0))\n = 0 -> no errors\n = 1 -> Assertion failed at assert(prevOwner == owner)\n = 3 -> Assertion failed at assert(owner == address(0) || y != z)\n diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy_indirect.sol b/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy_indirect.sol index 4ab3f21e6..1fcda01b0 100644 --- a/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy_indirect.sol +++ b/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy_indirect.sol @@ -43,5 +43,7 @@ contract C { // SMTEngine: all // SMTIgnoreCex: yes // ---- +// Warning 1218: (437-463): CHC: Error trying to invoke SMT solver. // Warning 6328: (419-433): CHC: Assertion violation happens here. -// Warning 6328: (437-463): CHC: Assertion violation happens here. +// Warning 6328: (437-463): CHC: Assertion violation might happen here. +// Warning 4661: (437-463): BMC: Assertion violation happens 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/functions_external_2.sol b/test/libsolidity/smtCheckerTests/functions/functions_external_2.sol index c2f55fa98..5efcb2da1 100644 --- a/test/libsolidity/smtCheckerTests/functions/functions_external_2.sol +++ b/test/libsolidity/smtCheckerTests/functions/functions_external_2.sol @@ -25,4 +25,4 @@ contract C // SMTIgnoreOS: macos // ---- // Warning 6328: (234-253): CHC: Assertion violation happens here. -// Info 1180: Reentrancy property(ies) for :C:\n!( = 1)\n((!((map[1] + ((- 1) * map[0])) >= 0) || ((map'[0] + ((- 1) * map'[1])) <= 0)) && (((map'[1] + ((- 1) * map'[0])) <= 0) || !((map[1] + ((- 1) * map[0])) <= 0)) && !( = 2))\n = 0 -> no errors\n = 1 -> Assertion failed at assert(map[0] == map[1])\n = 2 -> Assertion failed at assert(map[0] == map[1])\n = 3 -> Assertion failed at assert(map[0] == 0)\n +// Info 1180: Reentrancy property(ies) for :C:\n!( = 1)\n((!((map[1] + ((- 1) * map[0])) <= 0) || ((map'[1] + ((- 1) * map'[0])) <= 0)) && !( = 2) && (!((map[1] + ((- 1) * map[0])) >= 0) || ((map'[0] + ((- 1) * map'[1])) <= 0)))\n = 0 -> no errors\n = 1 -> Assertion failed at assert(map[0] == map[1])\n = 2 -> Assertion failed at assert(map[0] == map[1])\n = 3 -> Assertion failed at assert(map[0] == 0)\n diff --git a/test/libsolidity/smtCheckerTests/functions/virtual_function_called_by_constructor.sol b/test/libsolidity/smtCheckerTests/functions/virtual_function_called_by_constructor.sol index e30a5e743..0117f9b49 100644 --- a/test/libsolidity/smtCheckerTests/functions/virtual_function_called_by_constructor.sol +++ b/test/libsolidity/smtCheckerTests/functions/virtual_function_called_by_constructor.sol @@ -27,4 +27,4 @@ contract C is A { // ---- // Warning 6328: (199-214): CHC: Assertion violation happens here.\nCounterexample:\nx = 2\n\nTransaction trace:\nA.constructor()\nState: x = 2\nA.i() // Warning 6328: (387-401): CHC: Assertion violation happens here.\nCounterexample:\nx = 10\n\nTransaction trace:\nC.constructor()\nState: x = 10\nC.i() -// Info 1180: Contract invariant(s) for :A:\n(!(x <= 1) && !(x >= 3))\nContract invariant(s) for :C:\n(!(x <= 9) && !(x >= 11))\n +// Info 1180: Contract invariant(s) for :A:\n(!(x <= 1) && !(x >= 3))\nContract invariant(s) for :C:\n(!(x >= 11) && !(x <= 9))\n diff --git a/test/libsolidity/smtCheckerTests/operators/assignment_contract_member_variable.sol b/test/libsolidity/smtCheckerTests/operators/assignment_contract_member_variable.sol index 284f9bcbd..7a1deafe0 100644 --- a/test/libsolidity/smtCheckerTests/operators/assignment_contract_member_variable.sol +++ b/test/libsolidity/smtCheckerTests/operators/assignment_contract_member_variable.sol @@ -29,4 +29,4 @@ contract A { // SMTIgnoreCex: yes // ---- // Warning 6328: (392-408): CHC: Assertion violation happens here. -// Info 1180: Contract invariant(s) for :A:\n(((x = (- 2)) && (y = (- 2))) || ((x = 0) && (y = 0)))\n(((x = 0) && (y = 0)) || ((x = (- 2)) && (y = (- 2))))\n +// Info 1180: Contract invariant(s) for :A:\n(((x = (- 2)) && (y = (- 2))) || ((x = 0) && (y = 0)))\n 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/conditional_assignment_6.sol b/test/libsolidity/smtCheckerTests/operators/conditional_assignment_6.sol index 923147d49..b26fcbd93 100644 --- a/test/libsolidity/smtCheckerTests/operators/conditional_assignment_6.sol +++ b/test/libsolidity/smtCheckerTests/operators/conditional_assignment_6.sol @@ -25,4 +25,4 @@ contract C { // SMTIgnoreOS: macos // ---- // Warning 2072: (255-261): Unused local variable. -// Info 1180: Reentrancy property(ies) for :C:\n((!(x <= 2) || !(x' >= 3)) && ( <= 0) && (!(x' <= 0) || !(x >= 2)))\n = 0 -> no errors\n = 1 -> Assertion failed at assert(x == 2 || x == 1)\n +// Info 1180: Reentrancy property(ies) for :C:\n((!(x' >= 3) || (a' = a)) && ( <= 0) && (!(x' <= 0) || !(x >= 2)) && (!(x <= 2) || !(x' >= 3)))\n = 0 -> no errors\n = 1 -> Assertion failed at assert(x == 2 || x == 1)\n diff --git a/test/libsolidity/smtCheckerTests/special/tx_vars_reentrancy_1.sol b/test/libsolidity/smtCheckerTests/special/tx_vars_reentrancy_1.sol index 175b68410..7729cebb9 100644 --- a/test/libsolidity/smtCheckerTests/special/tx_vars_reentrancy_1.sol +++ b/test/libsolidity/smtCheckerTests/special/tx_vars_reentrancy_1.sol @@ -13,4 +13,4 @@ contract C { // SMTEngine: all // SMTIgnoreOS: macos // ---- -// Warning 6328: (135-169): CHC: Assertion violation happens here.\nCounterexample:\n\n_i = 0\nx = 2997\n\nTransaction trace:\nC.constructor()\nC.g(0){ msg.value: 2803 }\n _i.f() -- untrusted external call, synthesized as:\n C.g(0){ msg.value: 32278 } -- reentrant call\n _i.f() -- untrusted external call +// Warning 6328: (135-169): CHC: Assertion violation happens here.\nCounterexample:\n\n_i = 0\nx = 2997\n\nTransaction trace:\nC.constructor()\nC.g(0){ msg.value: 2803 }\n _i.f() -- untrusted external call, synthesized as:\n C.g(0){ msg.value: 2446 } -- reentrant call\n _i.f() -- untrusted external call diff --git a/test/libsolidity/smtCheckerTests/special/tx_vars_reentrancy_2.sol b/test/libsolidity/smtCheckerTests/special/tx_vars_reentrancy_2.sol index 81de958b3..e704cfd71 100644 --- a/test/libsolidity/smtCheckerTests/special/tx_vars_reentrancy_2.sol +++ b/test/libsolidity/smtCheckerTests/special/tx_vars_reentrancy_2.sol @@ -13,4 +13,6 @@ contract C { // SMTEngine: all // SMTIgnoreOS: macos // ---- -// Warning 6328: (157-191): CHC: Assertion violation happens here.\nCounterexample:\n\n_i = 0\nx = 101\n\nTransaction trace:\nC.constructor()\nC.g(0){ msg.value: 83 }\n _i.f{ value: 100 }() -- untrusted external call +// Warning 1218: (157-191): CHC: Error trying to invoke SMT solver. +// Warning 6328: (157-191): CHC: Assertion violation might happen here. +// Warning 4661: (157-191): BMC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/try_catch/try_public_var_mapping.sol b/test/libsolidity/smtCheckerTests/try_catch/try_public_var_mapping.sol index 2caae5e16..0854dedd1 100644 --- a/test/libsolidity/smtCheckerTests/try_catch/try_public_var_mapping.sol +++ b/test/libsolidity/smtCheckerTests/try_catch/try_public_var_mapping.sol @@ -21,5 +21,5 @@ contract C { // SMTEngine: all // SMTIgnoreOS: macos // ---- -// Warning 6328: (280-300): CHC: Assertion violation happens here. +// Warning 6328: (280-300): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f() // Info 1180: Contract invariant(s) for :C:\n!(m[0].length <= 1)\n(!(m[0][1] >= 43) && !(m[0][1] <= 41))\n diff --git a/test/libsolidity/smtCheckerTests/types/address_transfer_insufficient.sol b/test/libsolidity/smtCheckerTests/types/address_transfer_insufficient.sol index 4b55c3241..2fcdda175 100644 --- a/test/libsolidity/smtCheckerTests/types/address_transfer_insufficient.sol +++ b/test/libsolidity/smtCheckerTests/types/address_transfer_insufficient.sol @@ -11,6 +11,6 @@ contract C // ==== // SMTEngine: all // ---- -// Warning 6328: (180-204): CHC: Assertion violation happens here.\nCounterexample:\n\na = 0x2297\nb = 0x2297\n\nTransaction trace:\nC.constructor()\nC.f(0x2297, 0x2297) +// Warning 6328: (180-204): CHC: Assertion violation happens here.\nCounterexample:\n\na = 0x52f6\nb = 0x52f6\n\nTransaction trace:\nC.constructor()\nC.f(0x52f6, 0x52f6) // Warning 1236: (101-116): BMC: Insufficient funds happens here. // Warning 1236: (120-136): BMC: Insufficient funds happens here. diff --git a/test/libsolidity/smtCheckerTests/types/mapping_equal_keys_2.sol b/test/libsolidity/smtCheckerTests/types/mapping_equal_keys_2.sol index 0290d31e1..37e2e4c13 100644 --- a/test/libsolidity/smtCheckerTests/types/mapping_equal_keys_2.sol +++ b/test/libsolidity/smtCheckerTests/types/mapping_equal_keys_2.sol @@ -9,4 +9,4 @@ contract C // ==== // SMTEngine: all // ---- -// Warning 6328: (86-100): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 0\ny = 1\n\nTransaction trace:\nC.constructor()\nC.f(0, 1) +// Warning 6328: (86-100): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 1\ny = 0\n\nTransaction trace:\nC.constructor()\nC.f(1, 0) diff --git a/test/libsolidity/smtCheckerTests/types/static_array_length_1.sol b/test/libsolidity/smtCheckerTests/types/static_array_length_1.sol index e8b6f1a32..72bed0f4e 100644 --- a/test/libsolidity/smtCheckerTests/types/static_array_length_1.sol +++ b/test/libsolidity/smtCheckerTests/types/static_array_length_1.sol @@ -9,4 +9,4 @@ contract C { // SMTEngine: all // ---- // Warning 6328: (102-122): CHC: Assertion violation happens here.\nCounterexample:\n\na = [0x09, 0x09]\n\nTransaction trace:\nC.constructor()\nC.f([0x09, 0x09]) -// Warning 6328: (141-161): CHC: Assertion violation happens here.\nCounterexample:\n\na = [0x09, 0x09]\n\nTransaction trace:\nC.constructor()\nC.f([0x09, 0x09]) +// Warning 6328: (141-161): CHC: Assertion violation happens here.\nCounterexample:\n\na = [0x0a, 0x0a]\n\nTransaction trace:\nC.constructor()\nC.f([0x0a, 0x0a]) diff --git a/test/libsolidity/smtCheckerTests/types/struct/struct_aliasing_parameter_storage_2.sol b/test/libsolidity/smtCheckerTests/types/struct/struct_aliasing_parameter_storage_2.sol index 9d4623ae0..698262382 100644 --- a/test/libsolidity/smtCheckerTests/types/struct/struct_aliasing_parameter_storage_2.sol +++ b/test/libsolidity/smtCheckerTests/types/struct/struct_aliasing_parameter_storage_2.sol @@ -20,4 +20,4 @@ contract C { // ==== // SMTEngine: all // ---- -// Warning 6328: (289-322): CHC: Assertion violation happens here.\nCounterexample:\ns = {innerM, sum: 10}\n\nTransaction trace:\nC.constructor(0){ msg.sender: 0x6dc4 }\nState: s = {innerM, sum: 10}\nC.g(){ msg.sender: 0x0985 } +// Warning 6328: (289-322): CHC: Assertion violation happens here.\nCounterexample:\ns = {innerM, sum: 11}\n\nTransaction trace:\nC.constructor(0){ msg.sender: 0x6dc4 }\nState: s = {innerM, sum: 11}\nC.g(){ msg.sender: 0x0985 } diff --git a/test/libsolidity/smtCheckerTests/types/struct/struct_aliasing_parameter_storage_3.sol b/test/libsolidity/smtCheckerTests/types/struct/struct_aliasing_parameter_storage_3.sol index 8779cd095..fcf30555e 100644 --- a/test/libsolidity/smtCheckerTests/types/struct/struct_aliasing_parameter_storage_3.sol +++ b/test/libsolidity/smtCheckerTests/types/struct/struct_aliasing_parameter_storage_3.sol @@ -26,4 +26,4 @@ contract C { // ==== // SMTEngine: all // ---- -// Warning 6328: (307-327): CHC: Assertion violation happens here.\nCounterexample:\nt = {x: 10, s: {innerM, sum: 21239}}\n\nTransaction trace:\nC.constructor(0){ msg.sender: 0x6dc4 }\nState: t = {x: 10, s: {innerM, sum: 21239}}\nC.g() +// Warning 6328: (307-327): CHC: Assertion violation happens here.\nCounterexample:\nt = {x: 11, s: {innerM, sum: 21239}}\n\nTransaction trace:\nC.constructor(0){ msg.sender: 0x6dc4 }\nState: t = {x: 11, s: {innerM, sum: 21239}}\nC.g() diff --git a/test/libsolidity/smtCheckerTests/userTypes/fixedpoint.sol b/test/libsolidity/smtCheckerTests/userTypes/fixedpoint.sol index a8aa0bd9a..0a479c4ac 100644 --- a/test/libsolidity/smtCheckerTests/userTypes/fixedpoint.sol +++ b/test/libsolidity/smtCheckerTests/userTypes/fixedpoint.sol @@ -69,6 +69,6 @@ contract TestFixedMath { // SMTEngine: all // ---- // Warning 6328: (1886-1970): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nTestFixedMath.constructor()\nTestFixedMath.f()\n TestFixedMath.add(0, 0) -- internal call\n FixedMath.add(0, 0) -- internal call\n TestFixedMath.add(25, 45) -- internal call\n FixedMath.add(25, 45) -- internal call\n TestFixedMath.add(25, 45) -- internal call\n FixedMath.add(25, 45) -- internal call -// Warning 6328: (2165-2266): CHC: Assertion violation happens here. +// Warning 6328: (2165-2266): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nTestFixedMath.constructor()\nTestFixedMath.g()\n TestFixedMath.mul(340282366920938463463374607431768211456, 20) -- internal call\n FixedMath.mul(340282366920938463463374607431768211456, 20) -- internal call\n TestFixedMath.mul(340282366920938463463374607431768211456, 20) -- internal call\n FixedMath.mul(340282366920938463463374607431768211456, 20) -- internal call // Warning 6328: (2675-2791): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nTestFixedMath.constructor()\nTestFixedMath.h()\n TestFixedMath.floor(11579208923731619542357098500868790785326998665640564039457584007913129639930) -- internal call\n FixedMath.floor(11579208923731619542357098500868790785326998665640564039457584007913129639930) -- internal call\n TestFixedMath.floor(115792089237316195423570985008687907853269984665640564039457584007913129639935) -- internal call\n FixedMath.floor(115792089237316195423570985008687907853269984665640564039457584007913129639935) -- internal call\n TestFixedMath.floor(11579208923731619542357098500868790785326998665640564039457584007913129639930) -- internal call\n FixedMath.floor(11579208923731619542357098500868790785326998665640564039457584007913129639930) -- internal call // Warning 6328: (3161-3212): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nTestFixedMath.constructor()\nTestFixedMath.i()\n TestFixedMath.toUFixed256x18(0) -- internal call\n FixedMath.toUFixed256x18(0) -- internal call\n TestFixedMath.toUFixed256x18(5) -- internal call\n FixedMath.toUFixed256x18(5) -- internal call\n TestFixedMath.toUFixed256x18(115792089237316195423570985008687907853269984665640564039457) -- internal call\n FixedMath.toUFixed256x18(115792089237316195423570985008687907853269984665640564039457) -- internal call\n TestFixedMath.toUFixed256x18(5) -- internal call\n FixedMath.toUFixed256x18(5) -- internal call