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 #13439 from ethereum/z3_4_8_11_smt_tests

Browse Source 
Update SMT tests with z3 4.11.0
This commit is contained in:
Leo 2022-08-30 12:51:13 +02:00 committed by GitHub
commit e048ba4d75
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
36 changed files with 89 additions and 65 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

19
.circleci/config.yml
View File

@ -9,20 +9,20 @@ version: 2.1
parameters:
ubuntu-2004-docker-image:
type: string
# solbuildpackpusher/solidity-buildpack-deps:ubuntu2004-13
default: "solbuildpackpusher/solidity-buildpack-deps@sha256:aa64242ecba4f040a839eadfaf20e8489cf93d1cb96ab90df2b240cdbbfe7f7c"
# solbuildpackpusher/solidity-buildpack-deps:ubuntu2004-14
default: "solbuildpackpusher/solidity-buildpack-deps@sha256:d1ef23849db4c5462b248d89c111da4009b153cbd5002cb8755b0580312be581"
ubuntu-2004-clang-docker-image:
type: string
# solbuildpackpusher/solidity-buildpack-deps:ubuntu2004.clang-13
default: "solbuildpackpusher/solidity-buildpack-deps@sha256:caaf8d42aaf07397d1540e570f096a4fb1ef11fda7da3f1141d8852ec8322a9e"
# solbuildpackpusher/solidity-buildpack-deps:ubuntu2004.clang-14
default: "solbuildpackpusher/solidity-buildpack-deps@sha256:beb8c91998ec0df99a488900b3723a06f1122f0954fc73786b6c53fd73a6408d"
ubuntu-1604-clang-ossfuzz-docker-image:
type: string
# solbuildpackpusher/solidity-buildpack-deps:ubuntu1604.clang.ossfuzz-18
default: "solbuildpackpusher/solidity-buildpack-deps@sha256:048002d71a1f86f83dedb79dd057760b752256c75646ba5ad5c1bbe92e1695aa"
# solbuildpackpusher/solidity-buildpack-deps:ubuntu1604.clang.ossfuzz-19
default: "solbuildpackpusher/solidity-buildpack-deps@sha256:8c9bf1813c261d781f4c65fceed2dfb3ecf5be9ecf49bddbd250b570a7f3baea"
emscripten-docker-image:
type: string
# solbuildpackpusher/solidity-buildpack-deps:emscripten-12
default: "solbuildpackpusher/solidity-buildpack-deps@sha256:65a82268792a5a2ee85ad432baf04a056c3a4006941ab3a4416eb1a0614883f3"
# solbuildpackpusher/solidity-buildpack-deps:emscripten-13
default: "solbuildpackpusher/solidity-buildpack-deps@sha256:f1c13f3450d1f2e53ea18ac1ac1a17e932573cb9a5ccd0fd9ef6dd44f6402fa9"
evm-version:
type: string
default: london
@ -1087,6 +1087,9 @@ jobs:
environment:
EVM: << pipeline.parameters.evm-version >>
OPTIMIZE: 0
# The high parallelism in this job is causing the SMT tests to run out of memory,
# so disabling for now.
SOLTEST_FLAGS: --no-smt
<<: *steps_soltest
t_ubu_release_soltest_all: &t_ubu_release_soltest_all

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.17"
z3_version="4.11.0"
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" 189667930517aee07f1ce36485d5924a9a2cb4f8c3c9586b03e714a2c657541a
validate_checksum "$z3_package" b6a4a6d587e4bfb0643db81129f0f447692fae13d4bd1bd4d93f1c0301b75ffc
unzip "$z3_package"
rm "$z3_package"
cp "${z3_dir}/bin/libz3.a" /usr/local/lib

2
CMakeLists.txt
View File

@ -69,7 +69,7 @@ configure_file("${CMAKE_SOURCE_DIR}/cmake/templates/license.h.in" include/licens
include(EthOptions)
configure_project(TESTS)
set(LATEST_Z3_VERSION "4.8.17")
set(LATEST_Z3_VERSION "4.11.0")
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-12
# solbuildpackpusher/solidity-buildpack-deps:emscripten-13
docker run -v "$(pwd):/root/project" -w /root/project \
solbuildpackpusher/solidity-buildpack-deps@sha256:65a82268792a5a2ee85ad432baf04a056c3a4006941ab3a4416eb1a0614883f3 \
solbuildpackpusher/solidity-buildpack-deps@sha256:f1c13f3450d1f2e53ea18ac1ac1a17e932573cb9a5ccd0fd9ef6dd44f6402fa9 \
./scripts/ci/build_emscripten.sh "$BUILD_DIR"

5
test/libsolidity/smtCheckerTests/abi/abi_encode_packed_hash.sol
View File

@ -11,7 +11,6 @@ contract C {
}
// ====
// SMTEngine: all
// SMTIgnoreOS: macos
// ----
// Warning 1218: (281-319): CHC: Error trying to invoke SMT solver.
// Warning 6328: (281-319): CHC: Assertion violation might happen here.
// Warning 4661: (281-319): BMC: Assertion violation happens here.
// Warning 6328: (281-319): CHC: Assertion violation happens here.\nCounterexample:\n\na = 0\nb = 0\n\nTransaction trace:\nC.constructor()\nC.abiencodePackedHash(0, 0)

9
test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_hash.sol
View File

@ -13,11 +13,8 @@ contract C {
}
// ====
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 2072: (161-176): Unused local variable.
// Warning 1218: (379-417): CHC: Error trying to invoke SMT solver.
// Warning 1218: (436-474): CHC: Error trying to invoke SMT solver.
// Warning 6328: (379-417): CHC: Assertion violation might happen here.
// Warning 6328: (436-474): CHC: Assertion violation might happen here.
// Warning 4661: (379-417): BMC: Assertion violation happens here.
// Warning 4661: (436-474): BMC: Assertion violation happens here.
// Warning 6328: (379-417): CHC: Assertion violation happens here.
// Warning 6328: (436-474): CHC: Assertion violation happens here.

1
test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_vs_sig.sol
View File

@ -9,5 +9,6 @@ contract C {
// ====
// SMTEngine: all
// ----
// Warning 1218: (294-324): CHC: Error trying to invoke SMT solver.
// Warning 6328: (294-324): CHC: Assertion violation might happen here.
// Warning 7812: (294-324): BMC: Assertion violation might happen here.

4
test/libsolidity/smtCheckerTests/abi/abi_encode_with_sig_hash.sol
View File

@ -13,7 +13,5 @@ contract C {
// ====
// SMTEngine: all
// ----
// Warning 1218: (394-432): CHC: Error trying to invoke SMT solver.
// Warning 6328: (337-375): CHC: Assertion violation happens here.
// Warning 6328: (394-432): CHC: Assertion violation might happen here.
// Warning 4661: (394-432): BMC: Assertion violation happens here.
// Warning 6328: (394-432): CHC: Assertion violation happens here.

2
test/libsolidity/smtCheckerTests/abi/abi_encode_with_sig_simple.sol
View File

@ -25,7 +25,7 @@ contract C {
// ----
// Warning 5667: (107-122): Unused function parameter. Remove or comment out the variable name to silence this warning.
// Warning 1218: (824-854): CHC: Error trying to invoke SMT solver.
// Warning 6328: (543-573): CHC: Assertion violation happens here.
// Warning 6328: (543-573): CHC: Assertion violation happens here.\nCounterexample:\n\nt = false\nx = 0\ny = 0\nz = 0\nb5 = []\nb6 = []\n\nTransaction trace:\nC.constructor()\nC.abiEncodeSimple(sig, false, 0, 0, 0, a, b)
// Warning 6328: (664-694): CHC: Assertion violation happens here.
// Warning 6328: (713-743): CHC: Assertion violation happens here.
// Warning 6328: (824-854): CHC: Assertion violation might happen here.

3
test/libsolidity/smtCheckerTests/array_members/push_as_lhs_and_rhs_bytes.sol
View File

@ -12,5 +12,6 @@ contract C {
}
// ====
// SMTEngine: all
// SMTIgnoreOS: macos
// ----
// Warning 6328: (203-244): CHC: Assertion violation happens here.
// Warning 6328: (203-244): CHC: Assertion violation happens here.\nCounterexample:\nb = [0x0, 0x0]\nlength = 2\n\nTransaction trace:\nC.constructor()\nState: b = []\nC.f()

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/call_with_value_2.sol
View File

@ -11,5 +11,5 @@ contract C {
// ----
// Warning 9302: (96-116): Return value of low-level calls not used.
// Warning 6328: (120-156): CHC: Assertion violation might happen here.
// Warning 6328: (175-210): CHC: Assertion violation happens here.\nCounterexample:\n\ni = 0x0\n\nTransaction trace:\nC.constructor()\nC.g(0x0)\n i.call{value: 0}("") -- untrusted external call
// Warning 6328: (175-210): CHC: Assertion violation happens here.
// Warning 4661: (120-156): BMC: Assertion violation happens here.

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

@ -18,6 +18,7 @@ contract C {
}
// ====
// SMTEngine: all
// SMTIgnoreOS: macos
// ----
// 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()

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.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.g()\n C.h() -- trusted external call
// Warning 6328: (157-192): CHC: Assertion violation happens here.

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

@ -14,8 +14,6 @@ contract C {
// SMTEngine: all
// SMTIgnoreOS: macos
// ----
// Warning 1218: (202-236): CHC: Error trying to invoke SMT solver.
// Warning 6328: (150-183): CHC: Assertion violation might happen here.
// Warning 6328: (202-236): CHC: Assertion violation might happen here.
// Warning 6328: (202-236): CHC: Assertion violation happens here.\nCounterexample:\n\ni = 0\n\nTransaction trace:\nC.constructor()\nC.g(0)\n i.f{value: 20}() -- untrusted external call
// Warning 4661: (150-183): BMC: Assertion violation happens here.
// Warning 4661: (202-236): BMC: Assertion violation happens here.

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

@ -42,6 +42,4 @@ contract C {
// SMTIgnoreOS: macos
// ----
// Warning 2018: (33-88): Function state mutability can be restricted to view
// Warning 1218: (367-381): CHC: Error trying to invoke SMT solver.
// Warning 6328: (367-381): CHC: Assertion violation might happen here.
// Warning 4661: (367-381): BMC: Assertion violation happens here.
// Warning 6328: (367-381): CHC: Assertion violation happens here.

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

@ -44,5 +44,7 @@ contract C {
// 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.

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

@ -15,6 +15,7 @@ contract C {
}
// ====
// SMTEngine: all
// SMTIgnoreOS: macos
// ----
// Warning 1218: (206-220): CHC: Error trying to invoke SMT solver.
// Warning 6328: (206-220): CHC: Assertion violation might happen here.

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

@ -13,6 +13,4 @@ contract C {
// ====
// SMTEngine: all
// ----
// 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.
// 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

2
test/libsolidity/smtCheckerTests/function_selector/homer.sol
View File

@ -43,4 +43,4 @@ contract Homer is ERC165, Simpson {
// ====
// SMTEngine: all
// ----
// Warning 6328: (1340-1395): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nHomer.constructor()\nHomer.check()\n Homer.supportsInterface(0x73b6b492) -- internal call\n Homer.supportsInterface(0x01ffc9a7) -- internal call\n Homer.supportsInterface(0x8b9eb9ca) -- internal call
// Warning 6328: (1340-1395): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nHomer.constructor()\nHomer.supportsInterface(0x01ffc9a7)\nHomer.check()\n Homer.supportsInterface(0x73b6b492) -- internal call\n Homer.supportsInterface(0x01ffc9a7) -- internal call\n Homer.supportsInterface(0x8b9eb9ca) -- internal call

1
test/libsolidity/smtCheckerTests/functions/functions_storage_var_1_fail.sol
View File

@ -13,5 +13,6 @@ contract C
// ====
// SMTEngine: all
// SMTIgnoreOS: macos
// ----
// Warning 6328: (112-125): CHC: Assertion violation happens here.\nCounterexample:\na = 0\n\nTransaction trace:\nC.constructor()\nState: a = 0\nC.g()\n C.f(0) -- internal call

8
test/libsolidity/smtCheckerTests/imports/import_as_module_2.sol
View File

@ -18,5 +18,9 @@ function f(uint _x) pure {
// ====
// SMTEngine: all
// ----
// Warning 6328: (A:50-64): CHC: Assertion violation happens here.\nCounterexample:\n\n_y = 0\n\nTransaction trace:\nD.constructor()\nD.g(0)\n s1.sol:f(200) -- internal call\n s1.sol:f(0) -- internal call\n A:f(10) -- internal call\n A:f(0) -- internal call
// Warning 6328: (s1.sol:28-44): CHC: Assertion violation happens here.\nCounterexample:\n\n_y = 0\n\nTransaction trace:\nD.constructor()\nD.g(0)\n s1.sol:f(200) -- internal call\n s1.sol:f(0) -- internal call
// Warning 1218: (A:50-64): CHC: Error trying to invoke SMT solver.
// Warning 1218: (s1.sol:28-44): CHC: Error trying to invoke SMT solver.
// Warning 6328: (A:50-64): CHC: Assertion violation might happen here.
// Warning 6328: (s1.sol:28-44): CHC: Assertion violation might happen here.
// Warning 4661: (s1.sol:28-44): BMC: Assertion violation happens here.
// Warning 4661: (A:50-64): BMC: Assertion violation happens here.

2
test/libsolidity/smtCheckerTests/inheritance/receive_fallback.sol
View File

@ -21,6 +21,6 @@ contract B is A {
// ====
// SMTEngine: all
// ----
// Warning 6328: (87-101): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\nTransaction trace:\nA.constructor()\nState: x = 0\nA.receive(){ msg.value: 2 }
// Warning 6328: (87-101): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\nTransaction trace:\nA.constructor()\nState: x = 0\nA.receive(){ msg.value: 1 }
// Warning 6328: (136-150): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\nTransaction trace:\nA.constructor()\nState: x = 0\nA.g()
// Warning 6328: (255-269): CHC: Assertion violation happens here.\nCounterexample:\ny = 0, x = 0\n\nTransaction trace:\nB.constructor()\nState: y = 0, x = 0\nB.fallback()

4
test/libsolidity/smtCheckerTests/modifiers/modifier_inside_branch_assignment.sol
View File

@ -20,4 +20,6 @@ contract C {
// ====
// SMTEngine: all
// ----
// Warning 6328: (254-267): CHC: Assertion violation happens here.\nCounterexample:\nx = 0, owner = 0x0\ny = 1\n\nTransaction trace:\nC.constructor()\nState: x = 0, owner = 0x0\nC.g(1)\n C.f() -- internal call
// Warning 1218: (254-267): CHC: Error trying to invoke SMT solver.
// Warning 6328: (254-267): CHC: Assertion violation might happen here.
// Warning 4661: (254-267): BMC: Assertion violation happens here.

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

@ -12,4 +12,4 @@ contract C {
// SMTEngine: all
// SMTIgnoreOS: macos
// ----
// Warning 6328: (162-181): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 2\np = 0\n\nTransaction trace:\nC.constructor()\nC.f(2, 0)
// Warning 6328: (162-181): CHC: Assertion violation happens here.

3
test/libsolidity/smtCheckerTests/operators/compound_bitwise_string_literal_3.sol
View File

@ -18,5 +18,4 @@ contract C {
// SMTEngine: all
// ----
// Warning 6328: (229-276): CHC: Assertion violation happens here.\nCounterexample:\n\ny = 0x6062606464666060606260646466606060626064646660606062606464666060\nz = 0x6062606464666060606260646466606060626064646660606062606464666060\n\nTransaction trace:\nC.constructor()\nC.f()
// Warning 6328: (394-437): CHC: Assertion violation might happen here.
// Warning 4661: (394-437): BMC: Assertion violation happens here.
// Warning 6328: (394-437): CHC: Assertion violation happens here.\nCounterexample:\n\ny = 0x63666566676e616263666566676e616263666566676e616263666566676e6162\nz = 0x63666566676e616263666566676e616263666566676e616263666566676e6162\n\nTransaction trace:\nC.constructor()\nC.f()

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/overflow/signed_guard_sub_overflow.sol
View File

@ -8,4 +8,4 @@ contract C {
// SMTEngine: all
// SMTIgnoreOS: macos
// ----
// Warning 4984: (96-101): CHC: Overflow (resulting value larger than 0x80 * 2**248 - 1) happens here.\nCounterexample:\n\nx = 0\ny = (- 57896044618658097711785492504343953926634992332820282019728792003956564819968)\n = 0\n\nTransaction trace:\nC.constructor()\nC.f(0, (- 57896044618658097711785492504343953926634992332820282019728792003956564819968))
// Warning 4984: (96-101): CHC: Overflow (resulting value larger than 0x80 * 2**248 - 1) happens here.\nCounterexample:\n\nx = 57896044618658097711785492504343953926634992332820282019728792003956564819967\ny = (- 1)\n = 0\n\nTransaction trace:\nC.constructor()\nC.f(57896044618658097711785492504343953926634992332820282019728792003956564819967, (- 1))

2
test/libsolidity/smtCheckerTests/overflow/simple_overflow.sol
View File

@ -4,4 +4,4 @@ contract C {
// ====
// SMTEngine: all
// ----
// Warning 4984: (80-85): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\n\na = 1\nb = 115792089237316195423570985008687907853269984665640564039457584007913129639935\n = 0\n\nTransaction trace:\nC.constructor()\nC.f(1, 115792089237316195423570985008687907853269984665640564039457584007913129639935)
// Warning 4984: (80-85): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\n\na = 115792089237316195423570985008687907853269984665640564039457584007913129639935\nb = 1\n = 0\n\nTransaction trace:\nC.constructor()\nC.f(115792089237316195423570985008687907853269984665640564039457584007913129639935, 1)

3
test/libsolidity/smtCheckerTests/special/block_vars_chc_internal.sol
View File

@ -31,5 +31,6 @@ contract C {
}
// ====
// SMTEngine: chc
// SMTIgnoreOS: macos
// ----
// Warning 6328: (770-799): CHC: Assertion violation happens here.\nCounterexample:\ncoin = 0x1e28, dif = 0, gas = 0, number = 0, timestamp = 0\n\nTransaction trace:\nC.constructor()\nState: coin = 0x0, dif = 0, gas = 0, number = 0, timestamp = 0\nC.f(){ block.coinbase: 0x1e28, block.difficulty: 0, block.gaslimit: 0, block.number: 0, block.timestamp: 0 }\n C.g() -- internal call
// Warning 6328: (770-799): CHC: Assertion violation happens here.\nCounterexample:\ncoin = 0x0, dif = 0, gas = 0, number = 0, timestamp = 0\n\nTransaction trace:\nC.constructor()\nState: coin = 0x0, dif = 0, gas = 0, number = 0, timestamp = 0\nC.f(){ block.coinbase: 0x0, block.difficulty: 0, block.gaslimit: 0, block.number: 0, block.timestamp: 0 }\n C.g() -- internal call

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 = 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.\nCounterexample:\n\n_i = 0\nx = 868\n\nTransaction trace:\nC.constructor()\nC.g(0){ msg.value: 500 }\n _i.f() -- untrusted external call, synthesized as:\n C.g(0){ msg.value: 0 } -- reentrant call\n _i.f() -- untrusted external call

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

@ -21,4 +21,4 @@ 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()

8
test/libsolidity/smtCheckerTests/typecast/bytes_to_fixed_bytes_1.sol
View File

@ -3,20 +3,12 @@ contract C {
bytes memory b = hex"00010203040506070809000102030405060708090001020304050607080900010203040506070809";
bytes8 c = bytes8(b);
assert(c == 0x0001020304050607); // should hold
assert(c == 0x0001020304050608); // should fail
bytes16 d = bytes16(b);
assert(d == 0x00010203040506070809000102030405);
assert(d == 0x00010203040506070809000102030406); // should fail
bytes24 e = bytes24(b);
assert(e == 0x000102030405060708090001020304050607080900010203); // should hold
assert(e == 0x000102030405060708090001020304050607080900010204); // should fail
bytes32 g = bytes32(b);
assert(g == 0x0001020304050607080900010203040506070809000102030405060708090001); // should hold
assert(g == 0x0001020304050607080900010203040506070809000102030405060708090002); // should fail
}
}
// ----
// Warning 6328: (225-256): CHC: Assertion violation happens here.\nCounterexample:\n\nc = 0x01020304050607\nd = 0x0\ne = 0x0\ng = 0x0\n\nTransaction trace:\nC.constructor()\nC.f()
// Warning 6328: (352-399): CHC: Assertion violation happens here.\nCounterexample:\n\nc = 0x01020304050607\nd = 0x010203040506070809000102030405\ne = 0x0\ng = 0x0\n\nTransaction trace:\nC.constructor()\nC.f()
// Warning 6328: (526-589): CHC: Assertion violation happens here.\nCounterexample:\n\nc = 0x01020304050607\nd = 0x010203040506070809000102030405\ne = 0x0102030405060708090001020304050607080900010203\ng = 0x0\n\nTransaction trace:\nC.constructor()\nC.f()
// Warning 6328: (732-811): CHC: Assertion violation happens here.\nCounterexample:\n\nc = 0x01020304050607\nd = 0x010203040506070809000102030405\ne = 0x0102030405060708090001020304050607080900010203\ng = 0x01020304050607080900010203040506070809000102030405060708090001\n\nTransaction trace:\nC.constructor()\nC.f()

25
test/libsolidity/smtCheckerTests/typecast/bytes_to_fixed_bytes_1_fail.sol Normal file
View File

@ -0,0 +1,25 @@
contract C {
function f() external pure {
bytes memory b = hex"00010203040506070809000102030405060708090001020304050607080900010203040506070809";
bytes8 c = bytes8(b);
//assert(c == 0x0001020304050607); // should hold
assert(c == 0x0001020304050608); // should fail
bytes16 d = bytes16(b);
//assert(d == 0x00010203040506070809000102030405);
assert(d == 0x00010203040506070809000102030406); // should fail
bytes24 e = bytes24(b);
//assert(e == 0x000102030405060708090001020304050607080900010203); // should hold
assert(e == 0x000102030405060708090001020304050607080900010204); // should fail
bytes32 g = bytes32(b);
//assert(g == 0x0001020304050607080900010203040506070809000102030405060708090001); // should hold
assert(g == 0x0001020304050607080900010203040506070809000102030405060708090002); // should fail
}
}
// ====
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 6328: (227-258): CHC: Assertion violation happens here.
// Warning 6328: (356-403): CHC: Assertion violation happens here.
// Warning 6328: (532-595): CHC: Assertion violation happens here.
// Warning 6328: (740-819): 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()

4
test/libsolidity/smtCheckerTests/types/array_branch_1d.sol
View File

@ -12,4 +12,6 @@ contract C
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 6328: (143-159): CHC: Assertion violation happens here.
// Warning 1218: (143-159): CHC: Error trying to invoke SMT solver.
// Warning 6328: (143-159): CHC: Assertion violation might happen here.
// Warning 4661: (143-159): BMC: Assertion violation happens here.