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 #12521 from ethereum/smt_z3_4_14

Browse Source 
update smtchecker tests for new z3
This commit is contained in:
Daniel Kirchner 2022-01-12 19:26:03 +01:00 committed by GitHub
commit 81d3e532b8
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
31 changed files with 61 additions and 46 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

16
.circleci/config.yml
View File

@ -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

4
.circleci/osx_install_dependencies.sh
View File

@ -61,11 +61,11 @@ 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}"
validate_checksum "$z3_package" 191b26be2b617b2dffffce139d77abcd7e584859efbc10a58d01a1d7830697a4
validate_checksum "$z3_package" 1341671670e0c4e72da80815128a68975ee90816d50ceaf6bd820f06babe2cfd
unzip "$z3_package"
rm "$z3_package"
cp "${z3_dir}/bin/libz3.a" /usr/local/lib

2
CMakeLists.txt
View File

@ -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})

4
scripts/build_emscripten.sh
View File

@ -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"

5
test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_2.sol
View File

@ -14,7 +14,8 @@ contract C {
}
// ====
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// 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 4984: (266-272): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 6328: (235-273): CHC: Assertion violation happens here.
// Info 1180: Contract invariant(s) for :C:\nonce\n

2
test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_ext_calls_2.sol
View File

@ -9,7 +9,7 @@ contract C {
// ====
// SMTEngine: all
// SMTIgnoreCex: yes
// SMTIgnoreInv: yes
// ----
// 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(!(<errorCode> >= 2) && (((:var 1).balances[address(this)] + ((- 1) * (:var 0).balances[address(this)])) <= 0))\n<errorCode> = 0 -> no errors\n<errorCode> = 1 -> Assertion failed at assert(address(this).balance == x)\n<errorCode> = 2 -> Assertion failed at assert(address(this).balance >= x)\n

2
test/libsolidity/smtCheckerTests/control_flow/branches_with_return/branches_in_modifiers_2.sol
View File

@ -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

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

@ -21,6 +21,7 @@ contract C {
}
// ====
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 9302: (212-228): Return value of low-level calls not used.
// Warning 6328: (232-246): CHC: Assertion violation happens here.\nCounterexample:\nx = 1, lock = false\n_a = 0x0\ny = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0, lock = false\nC.f(0x0)\n _a.call("aaaaa") -- untrusted external call, synthesized as:\n C.set(1) -- reentrant call
// Warning 6328: (232-246): CHC: Assertion violation happens here.

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

@ -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.

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

@ -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()

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

@ -12,7 +12,8 @@ contract C {
}
// ====
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// 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.

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

@ -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) && !(<errorCode> = 1) && ((owner + ((- 1) * owner')) >= 0))\n<errorCode> = 0 -> no errors\n<errorCode> = 1 -> Assertion failed at assert(prevOwner == owner)\n<errorCode> = 3 -> Assertion failed at assert(owner == address(0) || y != z)\n
// Info 1180: Reentrancy property(ies) for :C:\n(((owner + ((- 1) * owner')) >= 0) && !(<errorCode> = 1) && ((owner + ((- 1) * owner')) <= 0))\n<errorCode> = 0 -> no errors\n<errorCode> = 1 -> Assertion failed at assert(prevOwner == owner)\n<errorCode> = 3 -> Assertion failed at assert(owner == address(0) || y != z)\n

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

@ -40,5 +40,4 @@ contract C {
}
// ====
// SMTEngine: all
// ----
// Info 1180: Contract invariant(s) for :C:\n((insidef || (z <= 0)) && (y <= 0))\nReentrancy property(ies) for :C:\n((!insidef || !(<errorCode> >= 2)) && (insidef' || !insidef) && (!(y <= 0) || (y' <= 0)))\n((!insidef || !(<errorCode> >= 3)) && (insidef' || !insidef))\n<errorCode> = 0 -> no errors\n<errorCode> = 2 -> Assertion failed at assert(z == y)\n<errorCode> = 3 -> Assertion failed at assert(prevOwner == owner)\n
// SMTIgnoreInv: yes

5
test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy_indirect.sol
View File

@ -42,6 +42,9 @@ contract C {
// ====
// SMTEngine: all
// SMTIgnoreCex: yes
// SMTIgnoreOS: macos
// ----
// 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.

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.

5
test/libsolidity/smtCheckerTests/file_level/import.sol
View File

@ -21,6 +21,7 @@ contract C {
}
// ====
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 6328: (B:238-252): CHC: Assertion violation happens here.\nCounterexample:\ndata = {x: 21238}\nx = 8\ny = 21238\n\nTransaction trace:\nC.constructor()\nState: data = {x: 0}\nC.g()\n C.f(7) -- internal call\n A:set({x: 0}, 7) -- internal call\n A:set({x: 8}, 8) -- internal call
// Warning 6328: (B:308-322): CHC: Assertion violation happens here.\nCounterexample:\ndata = {x: 6}\nx = 0\ny = 6\n\nTransaction trace:\nC.constructor()\nState: data = {x: 0}\nC.g()\n C.f(7) -- internal call\n A:set({x: 0}, 7) -- internal call\n A:set({x: 0}, 8) -- internal call
// Warning 6328: (B:238-252): CHC: Assertion violation happens here.
// Warning 6328: (B:308-322): CHC: Assertion violation happens here.

2
test/libsolidity/smtCheckerTests/functions/functions_external_2.sol
View File

@ -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!(<errorCode> = 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)) && !(<errorCode> = 2))\n<errorCode> = 0 -> no errors\n<errorCode> = 1 -> Assertion failed at assert(map[0] == map[1])\n<errorCode> = 2 -> Assertion failed at assert(map[0] == map[1])\n<errorCode> = 3 -> Assertion failed at assert(map[0] == 0)\n
// Info 1180: Reentrancy property(ies) for :C:\n!(<errorCode> = 1)\n((!((map[1] + ((- 1) * map[0])) <= 0) || ((map'[1] + ((- 1) * map'[0])) <= 0)) && !(<errorCode> = 2) && (!((map[1] + ((- 1) * map[0])) >= 0) || ((map'[0] + ((- 1) * map'[1])) <= 0)))\n<errorCode> = 0 -> no errors\n<errorCode> = 1 -> Assertion failed at assert(map[0] == map[1])\n<errorCode> = 2 -> Assertion failed at assert(map[0] == map[1])\n<errorCode> = 3 -> Assertion failed at assert(map[0] == 0)\n

2
test/libsolidity/smtCheckerTests/functions/virtual_function_called_by_constructor.sol
View File

@ -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

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

@ -27,6 +27,6 @@ contract A {
// ====
// SMTEngine: all
// SMTIgnoreCex: yes
// SMTIgnoreInv: 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

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)

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

@ -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)) && (<errorCode> <= 0) && (!(x' <= 0) || !(x >= 2)))\n<errorCode> = 0 -> no errors\n<errorCode> = 1 -> Assertion failed at assert(x == 2 || x == 1)\n
// Info 1180: Reentrancy property(ies) for :C:\n((!(x' >= 3) || (a' = a)) && (<errorCode> <= 0) && (!(x' <= 0) || !(x >= 2)) && (!(x <= 2) || !(x' >= 3)))\n<errorCode> = 0 -> no errors\n<errorCode> = 1 -> Assertion failed at assert(x == 2 || x == 1)\n

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

@ -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

4
test/libsolidity/smtCheckerTests/special/tx_vars_reentrancy_2.sol
View File

@ -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.

2
test/libsolidity/smtCheckerTests/try_catch/try_public_var_mapping.sol
View File

@ -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

3
test/libsolidity/smtCheckerTests/types/address_transfer_insufficient.sol
View File

@ -10,7 +10,8 @@ contract C
}
// ====
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// 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.
// Warning 1236: (101-116): BMC: Insufficient funds happens here.
// Warning 1236: (120-136): BMC: Insufficient funds happens here.

3
test/libsolidity/smtCheckerTests/types/mapping_equal_keys_2.sol
View File

@ -8,5 +8,6 @@ contract C
}
// ====
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// 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.

5
test/libsolidity/smtCheckerTests/types/static_array_length_1.sol
View File

@ -7,6 +7,7 @@ contract C {
}
// ====
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// 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: (102-122): CHC: Assertion violation happens here.
// Warning 6328: (141-161): CHC: Assertion violation happens here.

2
test/libsolidity/smtCheckerTests/types/struct/struct_aliasing_parameter_storage_2.sol
View File

@ -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 }

2
test/libsolidity/smtCheckerTests/types/struct/struct_aliasing_parameter_storage_3.sol
View File

@ -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()

3
test/libsolidity/smtCheckerTests/types/struct/struct_aliasing_parameter_storage_4.sol
View File

@ -25,5 +25,6 @@ contract C {
}
// ====
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 6328: (305-325): 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: (305-325): CHC: Assertion violation happens here.

7
test/libsolidity/smtCheckerTests/userTypes/fixedpoint.sol
View File

@ -67,8 +67,9 @@ contract TestFixedMath {
}
// ====
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// 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: (1886-1970): CHC: Assertion violation happens here.
// Warning 6328: (2165-2266): CHC: Assertion violation happens here.
// 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
// Warning 6328: (2675-2791): CHC: Assertion violation happens here.
// Warning 6328: (3161-3212): CHC: Assertion violation happens here.