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 #11673 from ethereum/smt_update_z3_12

Browse Source 
Update SMTChecker tests with z3 4.8.12
This commit is contained in:
Leonardo 2021-07-20 10:56:20 +02:00 committed by GitHub
commit d655a3c91b
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
33 changed files with 85 additions and 91 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-6
default: "solbuildpackpusher/solidity-buildpack-deps@sha256:da44d7f78e093f7f0415abf07f7c1fd1c2ed4fa65fefea428821a05186c42ec9"
# solbuildpackpusher/solidity-buildpack-deps:ubuntu2004-7
default: "solbuildpackpusher/solidity-buildpack-deps@sha256:af5a0c6ea5e113e477f5387955a862f9aea5cc74d9ceeb2377fc64e64088d200"
ubuntu-2004-clang-docker-image:
type: string
# solbuildpackpusher/solidity-buildpack-deps:ubuntu2004.clang-6
default: "solbuildpackpusher/solidity-buildpack-deps@sha256:c78dd9c48d393b57afe053aeb2d0d358a9f31ac85039a181724c2f8408d0bcf8"
# solbuildpackpusher/solidity-buildpack-deps:ubuntu2004.clang-7
default: "solbuildpackpusher/solidity-buildpack-deps@sha256:cb504c6456d4a2dd80b354acfd7429836da5acce4e394500c02d5740617f9d01"
ubuntu-1604-clang-ossfuzz-docker-image:
type: string
# solbuildpackpusher/solidity-buildpack-deps:ubuntu1604.clang.ossfuzz-9
default: "solbuildpackpusher/solidity-buildpack-deps@sha256:5078e1d74ab6f4329e9218c2d8c0ebe2d42817a3d4c3c62ce887100cbe9bc739"
# solbuildpackpusher/solidity-buildpack-deps:ubuntu1604.clang.ossfuzz-10
default: "solbuildpackpusher/solidity-buildpack-deps@sha256:ea15a35f6188360b425593c83e946660ab4ea4dac9b9c3bb3629e6ed57276b1d"
emscripten-docker-image:
type: string
# solbuildpackpusher/solidity-buildpack-deps:emscripten-5
default: "solbuildpackpusher/solidity-buildpack-deps@sha256:d28afb9624c2352ea40f157d1a321ffac77f54a21e33a8e8744f9126b780ded4"
# solbuildpackpusher/solidity-buildpack-deps:emscripten-6
default: "solbuildpackpusher/solidity-buildpack-deps@sha256:092da5817bc032c91a806b4f73db2a1a31e5cc4c066d94d43eedd9f365df7154"
orbs:
win: circleci/windows@2.2.0

16
.circleci/osx_install_dependencies.sh
View File

@ -48,13 +48,15 @@ then
./scripts/install_obsolete_jsoncpp_1_7_4.sh
# z3
wget https://github.com/Z3Prover/z3/releases/download/z3-4.8.10/z3-4.8.10-x64-osx-10.15.7.zip
unzip z3-4.8.10-x64-osx-10.15.7.zip
rm -f z3-4.8.10-x64-osx-10.15.7.zip
cp z3-4.8.10-x64-osx-10.15.7/bin/libz3.a /usr/local/lib
cp z3-4.8.10-x64-osx-10.15.7/bin/z3 /usr/local/bin
cp z3-4.8.10-x64-osx-10.15.7/include/* /usr/local/include
rm -rf z3-4.8.10-x64-osx-10.15.7
z3_version="z3-4.8.12"
osx_version="osx-10.15.7"
wget "https://github.com/Z3Prover/z3/releases/download/$z3_version/$z3_version-x64-$osx_version.zip"
unzip "$z3_version-x64-$osx_version.zip"
rm -f "$z3_version-x64-$osx_version.zip"
cp "$z3_version-x64-$osx_version/bin/libz3.a" /usr/local/lib
cp "$z3_version-x64-$osx_version/bin/z3" /usr/local/bin
cp "$z3_version-x64-$osx_version"/include/* /usr/local/include
rm -rf "$z3_version-x64-$osx_version"
# evmone
wget https://github.com/ethereum/evmone/releases/download/v0.7.0/evmone-0.7.0-darwin-x86_64.tar.gz

4
scripts/build_emscripten.sh
View File

@ -34,7 +34,7 @@ else
BUILD_DIR="$1"
fi
# solbuildpackpusher/solidity-buildpack-deps:emscripten-4
# solbuildpackpusher/solidity-buildpack-deps:emscripten-6
docker run -v "$(pwd):/root/project" -w /root/project \
solbuildpackpusher/solidity-buildpack-deps@sha256:434719d8104cab47712dd1f56f255994d04eb65b802c0d382790071c1a0c074b \
solbuildpackpusher/solidity-buildpack-deps@sha256:092da5817bc032c91a806b4f73db2a1a31e5cc4c066d94d43eedd9f365df7154 \
./scripts/ci/build_emscripten.sh "$BUILD_DIR"

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

@ -28,6 +28,7 @@ contract C {
}
// ====
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 2072: (643-658): Unused local variable.
// Warning 6328: (298-328): CHC: Assertion violation happens here.

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

@ -19,15 +19,13 @@ contract C {
// ====
// SMTEngine: all
// ----
// Warning 1218: (208-238): CHC: Error trying to invoke SMT solver.
// Warning 6328: (208-238): CHC: Assertion violation might happen here.
// Warning 6328: (208-238): CHC: Assertion violation happens here.
// Warning 1218: (286-316): CHC: Error trying to invoke SMT solver.
// Warning 6328: (286-316): CHC: Assertion violation might happen here.
// Warning 1218: (453-483): CHC: Error trying to invoke SMT solver.
// Warning 6328: (453-483): CHC: Assertion violation might happen here.
// Warning 1218: (532-562): CHC: Error trying to invoke SMT solver.
// Warning 6328: (532-562): CHC: Assertion violation might happen here.
// Warning 4661: (208-238): BMC: Assertion violation happens here.
// Warning 4661: (286-316): BMC: Assertion violation happens here.
// Warning 4661: (453-483): BMC: Assertion violation happens here.
// Warning 4661: (532-562): BMC: Assertion violation happens here.

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

@ -9,4 +9,5 @@ contract C {
// ====
// SMTEngine: all
// ----
// Warning 6328: (294-324): CHC: Assertion violation happens here.
// Warning 6328: (294-324): CHC: Assertion violation might happen here.
// Warning 7812: (294-324): BMC: Assertion violation might happen here.

2
test/libsolidity/smtCheckerTests/array_members/push_storage_ref_unsafe_aliasing.sol
View File

@ -14,5 +14,5 @@ contract C {
// SMTEngine: all
// ----
// Warning 6368: (188-192): CHC: Out of bounds access happens here.\nCounterexample:\na = []\nb = [32]\n\nTransaction trace:\nC.constructor()\nState: a = []\nC.f()
// Warning 6368: (188-195): CHC: Out of bounds access happens here.\nCounterexample:\na = [[], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [22, 22, 22, 22, 22, 22, 22, 22, 22, 22, 22, 22], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15]]\nb = [32]\n\nTransaction trace:\nC.constructor()\nState: a = []\nC.f()
// Warning 6368: (188-195): CHC: Out of bounds access happens here.\nCounterexample:\na = [[], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [25, 25, 25, 25, 25, 25, 25, 25], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15]]\nb = [32]\n\nTransaction trace:\nC.constructor()\nState: a = []\nC.f()
// Warning 6328: (181-202): CHC: Assertion violation happens here.\nCounterexample:\n\nb = [32]\n\nTransaction trace:\nC.constructor()\nState: a = []\nC.f()

22
test/libsolidity/smtCheckerTests/crypto/crypto_functions_fail.sol
View File

@ -7,12 +7,14 @@ contract C {
function s(bytes memory b0, bytes memory b1) public pure {
bytes32 s0 = sha256(b0);
bytes32 s1 = sha256(b1);
assert(s0 == s1);
// Disabled because of Spacer nondeterminism.
//assert(s0 == s1);
}
function r(bytes memory b0, bytes memory b1) public pure {
bytes32 r0 = ripemd160(b0);
bytes32 r1 = ripemd160(b1);
assert(r0 == r1);
// Disabled because of Spacer nondeterminism.
//assert(r0 == r1);
}
function e(bytes32 h0, uint8 v0, bytes32 r0, bytes32 s0, bytes32 h1, uint8 v1, bytes32 r1, bytes32 s1) public pure {
address a0 = ecrecover(h0, v0, r0, s0);
@ -25,12 +27,10 @@ contract C {
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 2072: (556-566): Unused local variable.
// Warning 2072: (598-608): Unused local variable.
// Warning 1218: (135-151): CHC: Error trying to invoke SMT solver.
// Warning 6328: (135-151): CHC: Assertion violation might happen here.
// Warning 6328: (272-288): CHC: Assertion violation happens here.
// Warning 1218: (415-431): CHC: Error trying to invoke SMT solver.
// Warning 6328: (415-431): CHC: Assertion violation might happen here.
// Warning 4661: (135-151): BMC: Assertion violation happens here.
// Warning 4661: (415-431): BMC: Assertion violation happens here.
// Warning 2072: (218-228): Unused local variable.
// Warning 2072: (245-255): Unused local variable.
// Warning 2072: (405-415): Unused local variable.
// Warning 2072: (435-445): Unused local variable.
// Warning 2072: (656-666): Unused local variable.
// Warning 2072: (698-708): Unused local variable.
// Warning 6328: (135-151): CHC: 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 = 3\n\nTransaction trace:\nC.constructor()\nState: s = 0, z = 3\nC.f()
// 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()

2
test/libsolidity/smtCheckerTests/file_level/constants_at_file_level_referencing.sol
View File

@ -58,7 +58,7 @@ contract C {
// ====
// SMTEngine: all
// ----
// Warning 6328: (s2.sol:518-539): CHC: Assertion violation happens here.\nCounterexample:\n\nr1 = [3, 1, 2]\nr2 = []\nr3 = []\nz = 0\n\nTransaction trace:\nC.constructor()\nC.p()\n C.f() -- internal call
// Warning 6328: (s2.sol:518-539): CHC: Assertion violation happens here.\nCounterexample:\n\nr2 = []\nr3 = []\nz = 0\n\nTransaction trace:\nC.constructor()\nC.p()\n C.f() -- internal call
// Warning 6328: (s2.sol:704-725): CHC: Assertion violation happens here.\nCounterexample:\n\nr1 = [3, 1, 2]\nr2 = [3, 1, 2]\nr3 = []\nz = 0\n\nTransaction trace:\nC.constructor()\nC.p()\n C.f() -- internal call\n C.g() -- internal call
// Warning 6328: (s2.sol:890-911): CHC: Assertion violation happens here.
// Warning 6328: (s2.sol:980-994): CHC: Assertion violation happens here.

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

@ -10,6 +10,7 @@ function fun(uint[] calldata _x, uint[] storage _y) view returns (uint, uint[]
}
// ====
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 4984: (168-180): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\ndata = []\nx = 1\n = 0\n = 0\na = 0\n\nTransaction trace:\nC.constructor()\nState: data = []\nC.f(1, input)\n fun(_x, []) -- internal call
// Warning 6368: (289-294): CHC: Out of bounds access happens here.\nCounterexample:\ndata = []\nx = 0\ninput = [5, 5, 5, 5, 5, 5, 5, 5, 5, 10, 5, 5, 13, 5, 5, 5, 5, 5, 19, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5]\n = 0\n = 0\n\nTransaction trace:\nC.constructor()\nState: data = []\nC.f(0, [5, 5, 5, 5, 5, 5, 5, 5, 5, 10, 5, 5, 13, 5, 5, 5, 5, 5, 19, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5])\n fun([5, 5, 5, 5, 5, 5, 5, 5, 5, 10, 5, 5, 13, 5, 5, 5, 5, 5, 19, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5], []) -- internal call
// Warning 4984: (168-180): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 6368: (289-294): CHC: Out of bounds access happens here.

2
test/libsolidity/smtCheckerTests/file_level/libraries_from_free.sol
View File

@ -23,6 +23,6 @@ contract C {
// ----
// Warning 4588: (190-197): Assertion checker does not yet implement this type of function call.
// Warning 4588: (190-197): Assertion checker does not yet implement this type of function call.
// Warning 6328: (284-298): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 8\ny = 8\n\nTransaction trace:\nC.constructor()\nC.f()\n fu() -- internal call\n L.inter() -- internal call
// Warning 6328: (284-298): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 0\ny = 8\n\nTransaction trace:\nC.constructor()\nC.f()\n fu() -- internal call\n L.inter() -- internal call
// Warning 6328: (363-377): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 0\ny = 8\n\nTransaction trace:\nC.constructor()\nC.f()\n fu() -- internal call\n L.inter() -- internal call
// Warning 4588: (190-197): Assertion checker does not yet implement this type of function call.

17
test/libsolidity/smtCheckerTests/file_level/recursion.sol
View File

@ -13,27 +13,16 @@ contract C {
}
function f() public pure {
// All of these should hold but the SMTChecker can't prove them.
// Disabled because of Spacer nondet
/*
assert(g(0, 0) == 1);
assert(g(0, 1) == 0);
assert(g(1, 0) == 1);
assert(g(2, 3) == 8);
assert(g(3, 10) == 59049);
*/
}
}
// ====
// SMTEngine: all
// ----
// Warning 4281: (118-130): CHC: Division by zero might happen here.
// Warning 4984: (134-148): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
// Warning 4984: (176-189): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
// Warning 6328: (430-450): CHC: Assertion violation happens here.
// Warning 6328: (478-498): CHC: Assertion violation might happen here.
// Warning 6328: (502-527): CHC: Assertion violation might happen here.
// Warning 2661: (134-148): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 2661: (176-189): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 2661: (134-148): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 2661: (134-148): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 8065: (176-189): BMC: Overflow (resulting value larger than 2**256 - 1) might happen here.
// Warning 4661: (478-498): BMC: Assertion violation happens here.
// Warning 2661: (134-148): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 4661: (502-527): BMC: Assertion violation happens here.

3
test/libsolidity/smtCheckerTests/functions/constructor_state_value.sol
View File

@ -12,5 +12,6 @@ contract C {
}
// ====
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 6328: (112-126): CHC: Assertion violation happens here.\nCounterexample:\nx = 10\ny = 11\n\nTransaction trace:\nC.constructor()\nState: x = 10\nC.f(11)
// Warning 6328: (112-126): CHC: Assertion violation happens here.

4
test/libsolidity/smtCheckerTests/functions/getters/bytes.sol
View File

@ -10,6 +10,4 @@ contract C {
// ====
// SMTEngine: all
// ----
// Warning 1218: (162-201): CHC: Error trying to invoke SMT solver.
// Warning 6328: (162-201): CHC: Assertion violation might happen here.
// Warning 4661: (162-201): BMC: Assertion violation happens here.
// Warning 6328: (162-201): CHC: Assertion violation happens here.

4
test/libsolidity/smtCheckerTests/functions/getters/string.sol
View File

@ -10,6 +10,4 @@ contract C {
// ====
// SMTEngine: all
// ----
// Warning 1218: (178-224): CHC: Error trying to invoke SMT solver.
// Warning 6328: (178-224): CHC: Assertion violation might happen here.
// Warning 4661: (178-224): BMC: Assertion violation happens here.
// Warning 6328: (178-224): CHC: Assertion violation happens here.

7
test/libsolidity/smtCheckerTests/inheritance/fallback_receive.sol
View File

@ -20,7 +20,8 @@ contract B is A {
}
// ====
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 6328: (81-95): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\nTransaction trace:\nA.constructor()\nState: x = 0\nA.fallback()
// Warning 6328: (130-144): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\nTransaction trace:\nA.constructor()\nState: x = 0\nA.g()
// Warning 6328: (256-270): CHC: Assertion violation happens here.\nCounterexample:\ny = 0, x = 0\n\nTransaction trace:\nB.constructor()\nState: y = 0, x = 0\nB.receive(){ value: 10450 }
// Warning 6328: (81-95): CHC: Assertion violation happens here.
// Warning 6328: (130-144): CHC: Assertion violation happens here.
// Warning 6328: (256-270): CHC: Assertion violation happens here.

7
test/libsolidity/smtCheckerTests/inheritance/receive.sol
View File

@ -20,7 +20,8 @@ contract B is A {
}
// ====
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 6328: (95-109): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\nTransaction trace:\nA.constructor()\nState: x = 0\nA.receive()
// Warning 6328: (144-158): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\nTransaction trace:\nA.constructor()\nState: x = 0\nA.g()
// Warning 6328: (267-281): CHC: Assertion violation happens here.\nCounterexample:\ny = 0, x = 0\n\nTransaction trace:\nB.constructor()\nState: y = 0, x = 0\nB.receive()
// Warning 6328: (95-109): CHC: Assertion violation happens here.
// Warning 6328: (144-158): CHC: Assertion violation happens here.
// Warning 6328: (267-281): CHC: Assertion violation happens here.

5
test/libsolidity/smtCheckerTests/inline_assembly/assembly_local_storage_access_inside_function.sol
View File

@ -17,8 +17,9 @@ contract C {
}
// ====
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 7737: (83-149): Inline assembly may cause SMTChecker to produce spurious warnings (false positives).
// Warning 6328: (152-167): CHC: Assertion violation happens here.\nCounterexample:\nz = 0\ni = 32\n\nTransaction trace:\nC.constructor()\nState: z = 0\nC.f()
// Warning 6328: (186-200): CHC: Assertion violation happens here.\nCounterexample:\nz = 0\ni = 32\n\nTransaction trace:\nC.constructor()\nState: z = 0\nC.f()
// Warning 6328: (152-167): CHC: Assertion violation happens here.
// Warning 6328: (186-200): CHC: Assertion violation happens here.
// Warning 7737: (83-149): Inline assembly may cause SMTChecker to produce spurious warnings (false positives).

2
test/libsolidity/smtCheckerTests/loops/while_nested_break_fail.sol
View File

@ -30,4 +30,4 @@ contract C
// SMTEngine: all
// ----
// Warning 6328: (296-311): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 0\ny = 10\nb = false\nc = true\n\nTransaction trace:\nC.constructor()\nC.f(0, 9, false, true)
// Warning 6328: (347-362): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 15\ny = 20\nb = false\nc = false\n\nTransaction trace:\nC.constructor()\nC.f(0, 0, false, false)
// Warning 6328: (347-362): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 15\ny = 0\nb = true\nc = false\n\nTransaction trace:\nC.constructor()\nC.f(9, 0, true, false)

11
test/libsolidity/smtCheckerTests/natspec/abstract_function_nondet_pow_no_abstraction.sol
View File

@ -7,6 +7,8 @@ contract C {
}
function pow(uint base, uint exponent) internal pure returns (uint) {
// Disabled because of Spacer nondet
/*
if (base == 0) {
return 0;
}
@ -28,16 +30,9 @@ contract C {
}
}
return base * y;
*/
}
}
// ====
// SMTEngine: chc
// ----
// Warning 4984: (176-179): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
// Warning 4281: (435-447): CHC: Division by zero might happen here.
// Warning 4984: (467-478): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
// Warning 4281: (495-507): CHC: Division by zero might happen here.
// Warning 4984: (529-537): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
// Warning 4984: (550-561): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
// Warning 3944: (579-591): CHC: Underflow (resulting value less than 0) might happen here.
// Warning 4984: (616-624): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.

2
test/libsolidity/smtCheckerTests/natspec/safe_assert_false_positive_pure.sol
View File

@ -26,4 +26,4 @@ contract C {
// ----
// Warning 2018: (33-335): Function state mutability can be restricted to view
// Warning 2018: (457-524): Function state mutability can be restricted to pure
// Warning 6328: (135-150): CHC: Assertion violation happens here.\nCounterexample:\nx = 0, y = 0\n_x = 0\nz = 1\nt = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0, y = 0\nC.g(0)\n C.f1(0) -- internal call
// Warning 6328: (135-150): CHC: Assertion violation happens here.\nCounterexample:\nx = 0, y = 0\n_x = 1\nz = 0\nt = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0, y = 0\nC.g(1)\n C.f1(1) -- internal call

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 = 115792089237316195423570985008687907853269984665640564039457584007913129639935\nb = 1\n = 0\n\nTransaction trace:\nC.constructor()\nC.f(115792089237316195423570985008687907853269984665640564039457584007913129639935, 1)
// 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)

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

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

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

@ -15,6 +15,6 @@ contract C {
// Warning 2072: (152-156): Unused local variable.
// Warning 8364: (123-124): Assertion checker does not yet implement type type(contract C)
// Warning 8364: (193-194): Assertion checker does not yet implement type type(contract C)
// Warning 6328: (220-236): CHC: Assertion violation happens here.\nCounterexample:\n\ndata = [13, 13, 13, 13, 13, 13, 13, 13, 10, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13]\na1 = 7719\nb1 = 5\nc1 = 6\na2 = 7719\nb2 = 5\nc2 = 6\n\nTransaction trace:\nC.constructor()\nC.f([13, 13, 13, 13, 13, 13, 13, 13, 10, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13])
// Warning 6328: (220-236): CHC: Assertion violation happens here.\nCounterexample:\n\ndata = [9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 13, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9]\na1 = 7719\nb1 = 5\nc1 = 6\na2 = 7719\nb2 = 5\nc2 = 6\n\nTransaction trace:\nC.constructor()\nC.f([9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 13, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9])
// Warning 8364: (123-124): Assertion checker does not yet implement type type(contract C)
// Warning 8364: (193-194): Assertion checker does not yet implement type type(contract C)

5
test/libsolidity/smtCheckerTests/special/blockhash.sol
View File

@ -9,6 +9,7 @@ contract C
}
// ====
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 6328: (52-76): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 38\ny = 0\n\nTransaction trace:\nC.constructor()\nC.f(38){ value: 8365 }
// Warning 6328: (80-104): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 38\ny = 0\n\nTransaction trace:\nC.constructor()\nC.f(38){ value: 32285 }
// Warning 6328: (52-76): CHC: Assertion violation happens here.
// Warning 6328: (80-104): CHC: Assertion violation happens here.

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

@ -27,4 +27,4 @@ contract C {
// ----
// Warning 6321: (247-251): Unnamed return variable can remain unassigned. Add an explicit return with value to all non-reverting code paths or name the variable.
// Warning 6321: (397-401): Unnamed return variable can remain unassigned. Add an explicit return with value to all non-reverting code paths or name the variable.
// Warning 6328: (407-416): CHC: Assertion violation happens here.\nCounterexample:\nx = false\n\nTransaction trace:\nC.constructor()\nState: x = true\nC.h()\n C.h_data() -- internal call\n C.h_data() -- internal call
// Warning 6328: (407-416): CHC: Assertion violation happens here.\nCounterexample:\nx = false\n\nTransaction trace:\nC.constructor()\nState: x = true\nC.h()\n C.h_data() -- internal call

5
test/libsolidity/smtCheckerTests/special/msg_data.sol
View File

@ -21,6 +21,7 @@ contract C
}
// ====
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 6328: (120-147): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f(){ value: 30612 }
// Warning 6328: (467-494): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.g(){ value: 30612 }
// Warning 6328: (120-147): CHC: Assertion violation happens here.
// Warning 6328: (467-494): CHC: Assertion violation happens here.

3
test/libsolidity/smtCheckerTests/try_catch/try_multiple_catch_clauses_2.sol
View File

@ -19,5 +19,6 @@ contract C {
}
// ====
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 6328: (306-320): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 3\nsuccess = false\n\nTransaction trace:\nC.constructor()\nC.f()
// Warning 6328: (306-320): CHC: Assertion violation happens here.

1
test/libsolidity/smtCheckerTests/types/array_aliasing_storage_5.sol
View File

@ -33,6 +33,7 @@ contract C
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 6368: (186-196): CHC: Out of bounds access might happen here.
// Warning 6368: (329-333): CHC: Out of bounds access happens here.
// Warning 6368: (342-346): CHC: Out of bounds access happens here.
// Warning 6368: (355-359): CHC: Out of bounds access happens here.

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

@ -9,6 +9,7 @@ contract C {
}
// ====
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 6328: (114-133): CHC: Assertion violation happens here.\nCounterexample:\n\n_x = 0\ny = 0\nz = 0\n\nTransaction trace:\nC.constructor()\nC.f(0)
// Warning 6328: (137-157): CHC: Assertion violation happens here.\nCounterexample:\n\n_x = 52647538830022687173130149211684818290356179572910782152375644828738034597888\ny = 52647538830022687173130149211684818290356179572910782152375644828738034597888\nz = 52647538830022687173130149211684818290356179572910782152375644828738034597888\n\nTransaction trace:\nC.constructor()\nC.f(52647538830022687173130149211684818290356179572910782152375644828738034597888)
// Warning 6328: (114-133): CHC: Assertion violation happens here.
// Warning 6328: (137-157): CHC: Assertion violation happens here.

1
test/libsolidity/smtCheckerTests/types/struct/struct_array_struct_array_memory_unsafe_2.sol
View File

@ -36,5 +36,6 @@ contract C {
}
// ====
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 6328: (804-842): CHC: Assertion violation happens here.

7
test/libsolidity/smtCheckerTests/types/struct/struct_array_struct_array_storage_unsafe_1.sol
View File

@ -40,9 +40,10 @@ contract C {
}
// ====
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 6328: (148-165): CHC: Assertion violation happens here.
// Warning 6328: (183-202): CHC: Assertion violation happens here.\nCounterexample:\ns1 = {x: 2, t: {y: 3, a: []}, a: [], ts: []}\n\nTransaction trace:\nC.constructor()\nState: s1 = {x: 0, t: {y: 0, a: []}, a: [], ts: []}\nC.f()
// Warning 6328: (183-202): CHC: Assertion violation happens here.
// Warning 6328: (266-286): CHC: Assertion violation happens here.
// Warning 6328: (404-427): CHC: Assertion violation happens here.\nCounterexample:\ns1 = {x: 2, t: {y: 3, a: []}, a: [0, 0, 4], ts: [{y: 0, a: []}, {y: 0, a: []}, {y: 0, a: []}, {y: 5, a: []}, {y: 0, a: []}, {y: 0, a: []}]}\n\nTransaction trace:\nC.constructor()\nState: s1 = {x: 0, t: {y: 0, a: []}, a: [], ts: []}\nC.f()
// Warning 6328: (578-604): CHC: Assertion violation happens here.\nCounterexample:\ns1 = {x: 2, t: {y: 3, a: []}, a: [0, 0, 4], ts: [{y: 0, a: []}, {y: 0, a: []}, {y: 0, a: []}, {y: 5, a: []}, {y: 0, a: [0, 0, 0, 0, 0, 6]}, {y: 0, a: []}]}\n\nTransaction trace:\nC.constructor()\nState: s1 = {x: 0, t: {y: 0, a: []}, a: [], ts: []}\nC.f()
// Warning 6328: (404-427): CHC: Assertion violation happens here.
// Warning 6328: (578-604): CHC: Assertion violation happens here.