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 #13740 from ethereum/z3_4_11_2_tests

Browse Source 
update SMTChecker tests with Z3 4.11.2
This commit is contained in:
Leo 2022-11-24 14:25:56 +01:00 committed by GitHub
commit a00e6c6089
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
75 changed files with 141 additions and 295 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-15
default: "solbuildpackpusher/solidity-buildpack-deps@sha256:e4f83457bf1d6475c3189e9013da77289793a5ecd6a0e15dbec9411880b11e22"
# solbuildpackpusher/solidity-buildpack-deps:ubuntu2004-16
default: "solbuildpackpusher/solidity-buildpack-deps@sha256:ee1def5806f40c35d583234e172ec5769bb9a08b6f5bbc713c1a2658846dbced"
ubuntu-2004-clang-docker-image:
type: string
# solbuildpackpusher/solidity-buildpack-deps:ubuntu2004.clang-15
default: "solbuildpackpusher/solidity-buildpack-deps@sha256:8dda4fdae312f840fbb4e25b9ef01ad3209e9014e49e4564ab0f0d2510225131"
# solbuildpackpusher/solidity-buildpack-deps:ubuntu2004.clang-16
default: "solbuildpackpusher/solidity-buildpack-deps@sha256:8f635529a10e0ddf955d6d72360261966e5fee0b5c5211070370ca2fc4e0ab7c"
ubuntu-1604-clang-ossfuzz-docker-image:
type: string
# solbuildpackpusher/solidity-buildpack-deps:ubuntu1604.clang.ossfuzz-20
default: "solbuildpackpusher/solidity-buildpack-deps@sha256:7b3ccaed3b5d37dc2cc4bbe1a1e40949266292dcdbc3ad015271ab4e5e6f5038"
# solbuildpackpusher/solidity-buildpack-deps:ubuntu1604.clang.ossfuzz-21
default: "solbuildpackpusher/solidity-buildpack-deps@sha256:ae6b695fb8a0806702bb6a1a9616fbb33ac3288f25990fa799aab2c045c80ea1"
emscripten-docker-image:
type: string
# solbuildpackpusher/solidity-buildpack-deps:emscripten-13
default: "solbuildpackpusher/solidity-buildpack-deps@sha256:f1c13f3450d1f2e53ea18ac1ac1a17e932573cb9a5ccd0fd9ef6dd44f6402fa9"
# solbuildpackpusher/solidity-buildpack-deps:emscripten-14
default: "solbuildpackpusher/solidity-buildpack-deps@sha256:d7d4ec28cdc3e61fc6a048b88ebdff1c5e67f3353cf1739cbaea07ec2481eb16"
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.11.0"
z3_version="4.11.2"
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" b6a4a6d587e4bfb0643db81129f0f447692fae13d4bd1bd4d93f1c0301b75ffc
validate_checksum "$z3_package" a56b6c40d9251a963aabe1f15731dd88ad1cb801d0e7b16e45f8b232175e165c
unzip "$z3_package"
rm "$z3_package"
cp "${z3_dir}/bin/libz3.a" /usr/local/lib

2
CMakeLists.txt
View File

@ -75,7 +75,7 @@ configure_file("${CMAKE_SOURCE_DIR}/cmake/templates/license.h.in" include/licens
include(EthOptions)
configure_project(TESTS)
set(LATEST_Z3_VERSION "4.11.0")
set(LATEST_Z3_VERSION "4.11.2")
set(MINIMUM_Z3_VERSION "4.8.0")
find_package(Z3)
if (${Z3_FOUND})

2
scripts/build_emscripten.sh
View File

@ -34,7 +34,7 @@ else
BUILD_DIR="$1"
fi
# solbuildpackpusher/solidity-buildpack-deps:emscripten-13
# solbuildpackpusher/solidity-buildpack-deps:emscripten-14
# NOTE: Without `safe.directory` git would assume it's not safe to operate on /root/project since it's owned by a different user.
# See https://github.blog/2022-04-12-git-security-vulnerability-announced/
docker run -v "$(pwd):/root/project" -w /root/project \

4
scripts/error_codes.py
View File

@ -227,10 +227,10 @@ def examine_id_coverage(top_dir, source_id_to_file_names, new_ids_only=False):
return False
old_source_only_ids = {
"1584", "1823",
"1218", "1584", "1823",
"1988", "2066", "2833", "3356",
"3893", "3996", "4010", "4458", "4802",
"4902", "5272", "5622", "5798", "7128", "7400",
"4902", "5272", "5622", "5798", "5840", "7128", "7400",
"7589", "7593", "7649", "7710",
"8065", "8084", "8140", "8158",
"8312", "8592", "9134", "9609",

4
test/cmdlineTests/model_checker_invariants_all/err
View File

@ -5,8 +5,8 @@ Warning: Return value of low-level calls not used.
| ^^^^^^^^^^^
Info: Contract invariant(s) for model_checker_invariants_all/input.sol:test:
((x <= 0) || true)
(!(x >= 1) || true)
Reentrancy property(ies) for model_checker_invariants_all/input.sol:test:
(((!(x <= 0) || (x' <= 0)) && (!(x <= 0) || (<errorCode> <= 0))) || true)
(((!(x <= 0) || !(x' >= 1)) && (!(x <= 0) || !(<errorCode> >= 1))) || true)
<errorCode> = 0 -> no errors
<errorCode> = 1 -> Assertion failed at assert(x == 0)

2
test/cmdlineTests/model_checker_invariants_contract/err
View File

@ -1,2 +1,2 @@
Info: Contract invariant(s) for model_checker_invariants_contract/input.sol:test:
((x <= 0) || true)
(!(x >= 1) || true)

4
test/cmdlineTests/model_checker_invariants_contract_reentrancy/err
View File

@ -5,8 +5,8 @@ Warning: Return value of low-level calls not used.
| ^^^^^^^^^^^
Info: Contract invariant(s) for model_checker_invariants_contract_reentrancy/input.sol:test:
((x <= 0) || true)
(!(x >= 1) || true)
Reentrancy property(ies) for model_checker_invariants_contract_reentrancy/input.sol:test:
(((!(x <= 0) || (x' <= 0)) && (!(x <= 0) || (<errorCode> <= 0))) || true)
(((!(x <= 0) || !(x' >= 1)) && (!(x <= 0) || !(<errorCode> >= 1))) || true)
<errorCode> = 0 -> no errors
<errorCode> = 1 -> Assertion failed at assert(x == 0)

2
test/cmdlineTests/model_checker_invariants_reentrancy/err
View File

@ -5,6 +5,6 @@ Warning: Return value of low-level calls not used.
| ^^^^^^^^^^^
Info: Reentrancy property(ies) for model_checker_invariants_reentrancy/input.sol:test:
(((!(x <= 0) || (x' <= 0)) && (!(x <= 0) || (<errorCode> <= 0))) || true)
(((!(x <= 0) || !(x' >= 1)) && (!(x <= 0) || !(<errorCode> >= 1))) || true)
<errorCode> = 0 -> no errors
<errorCode> = 1 -> Assertion failed at assert(x < 10)

4
test/cmdlineTests/standard_model_checker_invariants_contract/output.json
View File

@ -5,12 +5,12 @@
"component": "general",
"errorCode": "1180",
"formattedMessage": "Info: Contract invariant(s) for A:test:
((x <= 0) || true)
(!(x >= 1) || true)
",
"message": "Contract invariant(s) for A:test:
((x <= 0) || true)
(!(x >= 1) || true)
",
"severity": "info",
"type": "Info"

4
test/cmdlineTests/standard_model_checker_invariants_reentrancy/output.json
View File

@ -25,14 +25,14 @@
"component": "general",
"errorCode": "1180",
"formattedMessage": "Info: Reentrancy property(ies) for A:test:
(((!(x <= 0) || (x' <= 0)) && (!(x <= 0) || (<errorCode> <= 0))) || true)
(((!(x <= 0) || !(x' >= 1)) && (!(x <= 0) || !(<errorCode> >= 1))) || true)
<errorCode> = 0 -> no errors
<errorCode> = 1 -> Assertion failed at assert(x < 10)
",
"message": "Reentrancy property(ies) for A:test:
(((!(x <= 0) || (x' <= 0)) && (!(x <= 0) || (<errorCode> <= 0))) || true)
(((!(x <= 0) || !(x' >= 1)) && (!(x <= 0) || !(<errorCode> >= 1))) || true)
<errorCode> = 0 -> no errors
<errorCode> = 1 -> Assertion failed at assert(x < 10)
",

6
test/libsolidity/SMTCheckerTest.cpp
View File

@ -38,10 +38,8 @@ SMTCheckerTest::SMTCheckerTest(string const& _filename): SyntaxTest(_filename, E
BOOST_THROW_EXCEPTION(runtime_error("Invalid SMT \"show unproved\" choice."));
m_modelCheckerSettings.solvers = smtutil::SMTSolverChoice::None();
auto const& choice = m_reader.stringSetting("SMTSolvers", "any");
if (choice == "any")
m_modelCheckerSettings.solvers = smtutil::SMTSolverChoice::All();
else if (choice == "none")
auto const& choice = m_reader.stringSetting("SMTSolvers", "z3");
if (choice == "none")
m_modelCheckerSettings.solvers = smtutil::SMTSolverChoice::None();
else if (!m_modelCheckerSettings.solvers.setSolver(choice))
BOOST_THROW_EXCEPTION(runtime_error("Invalid SMT solver choice."));

8
test/libsolidity/smtCheckerTests/abi/abi_decode_simple.sol
View File

@ -21,14 +21,10 @@ contract C {
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 1218: (505-519): CHC: Error trying to invoke SMT solver.
// Warning 1218: (538-552): CHC: Error trying to invoke SMT solver.
// Warning 6328: (209-223): CHC: Assertion violation happens here.
// Warning 6328: (260-274): CHC: Assertion violation happens here.
// Warning 6328: (359-373): CHC: Assertion violation happens here.
// Warning 6328: (392-406): CHC: Assertion violation happens here.
// Warning 6328: (425-434): CHC: Assertion violation happens here.
// Warning 6328: (505-519): CHC: Assertion violation might happen here.
// Warning 6328: (538-552): CHC: Assertion violation might happen here.
// Warning 4661: (505-519): BMC: Assertion violation happens here.
// Warning 4661: (538-552): BMC: Assertion violation happens here.
// Warning 6328: (505-519): CHC: Assertion violation happens here.
// Warning 6328: (538-552): CHC: Assertion violation happens here.

16
test/libsolidity/smtCheckerTests/abi/abi_encode_packed_simple.sol
View File

@ -23,15 +23,7 @@ contract C {
// ====
// SMTEngine: all
// ----
// Warning 1218: (322-352): CHC: Error trying to invoke SMT solver.
// Warning 1218: (419-449): CHC: Error trying to invoke SMT solver.
// Warning 1218: (528-558): CHC: Error trying to invoke SMT solver.
// Warning 1218: (577-607): CHC: Error trying to invoke SMT solver.
// Warning 6328: (322-352): CHC: Assertion violation might happen here.
// Warning 6328: (419-449): CHC: Assertion violation might happen here.
// Warning 6328: (528-558): CHC: Assertion violation might happen here.
// Warning 6328: (577-607): CHC: Assertion violation might happen here.
// Warning 4661: (322-352): BMC: Assertion violation happens here.
// Warning 4661: (419-449): BMC: Assertion violation happens here.
// Warning 4661: (528-558): BMC: Assertion violation happens here.
// Warning 4661: (577-607): BMC: Assertion violation happens here.
// Warning 6328: (322-352): CHC: Assertion violation happens here.\nCounterexample:\n\nt = false\nx = 0\ny = 0\nz = 0\nb4 = []\nb5 = []\n\nTransaction trace:\nC.constructor()\nC.abiencodePackedSimple(false, 0, 0, 0, a, b)
// Warning 6328: (419-449): CHC: Assertion violation happens here.\nCounterexample:\n\nt = false\nx = 0\ny = 0\nz = 0\nb5 = []\n\nTransaction trace:\nC.constructor()\nC.abiencodePackedSimple(false, 0, 0, 0, a, b)
// Warning 6328: (528-558): CHC: Assertion violation happens here.\nCounterexample:\n\nt = false\nx = 0\ny = 0\nz = 0\n\nTransaction trace:\nC.constructor()\nC.abiencodePackedSimple(false, 0, 0, 0, a, b)
// Warning 6328: (577-607): CHC: Assertion violation happens here.\nCounterexample:\n\nt = false\nx = 0\ny = 0\nz = 0\n\nTransaction trace:\nC.constructor()\nC.abiencodePackedSimple(false, 0, 0, 0, a, b)

21
test/libsolidity/smtCheckerTests/abi/abi_encode_packed_string_literal.sol
View File

@ -21,19 +21,10 @@ contract C {
}
// ====
// SMTEngine: all
// SMTIgnoreOS: macos
// ----
// Warning 1218: (226-256): CHC: Error trying to invoke SMT solver.
// Warning 1218: (310-340): CHC: Error trying to invoke SMT solver.
// Warning 1218: (483-513): CHC: Error trying to invoke SMT solver.
// Warning 1218: (568-598): CHC: Error trying to invoke SMT solver.
// Warning 1218: (654-684): CHC: Error trying to invoke SMT solver.
// Warning 6328: (226-256): CHC: Assertion violation might happen here.
// Warning 6328: (310-340): CHC: Assertion violation might happen here.
// Warning 6328: (483-513): CHC: Assertion violation might happen here.
// Warning 6328: (568-598): CHC: Assertion violation might happen here.
// Warning 6328: (654-684): CHC: Assertion violation might happen here.
// Warning 4661: (226-256): BMC: Assertion violation happens here.
// Warning 4661: (310-340): BMC: Assertion violation happens here.
// Warning 4661: (483-513): BMC: Assertion violation happens here.
// Warning 4661: (568-598): BMC: Assertion violation happens here.
// Warning 4661: (654-684): BMC: Assertion violation happens here.
// Warning 6328: (226-256): CHC: Assertion violation happens here.\nCounterexample:\n\nb1 = [0x42, 0x42, 0x42, 0x42, 0x42, 0x42, 0x42, 0x42, 0x42, 0x42, 0x42, 0x42, 0x42, 0x42, 0x42, 0x42, 0x42, 0x42, 0x42]\nb3 = []\nb4 = []\nb5 = []\nb6 = []\n\nTransaction trace:\nC.constructor()\nC.abiencodePackedStringLiteral()
// Warning 6328: (310-340): CHC: Assertion violation happens here.\nCounterexample:\n\nb2 = [0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72]\nb4 = []\nb5 = []\nb6 = []\n\nTransaction trace:\nC.constructor()\nC.abiencodePackedStringLiteral()
// Warning 6328: (483-513): CHC: Assertion violation happens here.\nCounterexample:\n\nb5 = []\nb6 = []\n\nTransaction trace:\nC.constructor()\nC.abiencodePackedStringLiteral()
// Warning 6328: (568-598): CHC: Assertion violation happens here.\nCounterexample:\n\nb2 = [0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc]\nb6 = []\n\nTransaction trace:\nC.constructor()\nC.abiencodePackedStringLiteral()
// Warning 6328: (654-684): CHC: Assertion violation happens here.\nCounterexample:\n\nb3 = [0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a]\nb6 = [0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117]\n\nTransaction trace:\nC.constructor()\nC.abiencodePackedStringLiteral()

17
test/libsolidity/smtCheckerTests/abi/abi_encode_packed_string_literal_no_unproved.sol
View File

@ -22,15 +22,10 @@ contract C {
// ====
// SMTEngine: all
// SMTShowUnproved: no
// SMTIgnoreOS: macos
// ----
// Warning 1218: (226-256): CHC: Error trying to invoke SMT solver.
// Warning 1218: (310-340): CHC: Error trying to invoke SMT solver.
// Warning 1218: (483-513): CHC: Error trying to invoke SMT solver.
// Warning 1218: (568-598): CHC: Error trying to invoke SMT solver.
// Warning 1218: (654-684): CHC: Error trying to invoke SMT solver.
// Warning 5840: CHC: 5 verification condition(s) could not be proved. Enable the model checker option "show unproved" to see all of them. Consider choosing a specific contract to be verified in order to reduce the solving problems. Consider increasing the timeout per query.
// Warning 4661: (226-256): BMC: Assertion violation happens here.
// Warning 4661: (310-340): BMC: Assertion violation happens here.
// Warning 4661: (483-513): BMC: Assertion violation happens here.
// Warning 4661: (568-598): BMC: Assertion violation happens here.
// Warning 4661: (654-684): BMC: Assertion violation happens here.
// Warning 6328: (226-256): CHC: Assertion violation happens here.\nCounterexample:\n\nb1 = [0x42, 0x42, 0x42, 0x42, 0x42, 0x42, 0x42, 0x42, 0x42, 0x42, 0x42, 0x42, 0x42, 0x42, 0x42, 0x42, 0x42, 0x42, 0x42]\nb3 = []\nb4 = []\nb5 = []\nb6 = []\n\nTransaction trace:\nC.constructor()\nC.abiencodePackedStringLiteral()
// Warning 6328: (310-340): CHC: Assertion violation happens here.\nCounterexample:\n\nb2 = [0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72]\nb4 = []\nb5 = []\nb6 = []\n\nTransaction trace:\nC.constructor()\nC.abiencodePackedStringLiteral()
// Warning 6328: (483-513): CHC: Assertion violation happens here.\nCounterexample:\n\nb5 = []\nb6 = []\n\nTransaction trace:\nC.constructor()\nC.abiencodePackedStringLiteral()
// Warning 6328: (568-598): CHC: Assertion violation happens here.\nCounterexample:\n\nb2 = [0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc]\nb6 = []\n\nTransaction trace:\nC.constructor()\nC.abiencodePackedStringLiteral()
// Warning 6328: (654-684): CHC: Assertion violation happens here.\nCounterexample:\n\nb3 = [0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a]\nb6 = [0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117]\n\nTransaction trace:\nC.constructor()\nC.abiencodePackedStringLiteral()

13
test/libsolidity/smtCheckerTests/abi/abi_encode_simple.sol
View File

@ -19,13 +19,8 @@ contract C {
}
// ====
// SMTEngine: all
// SMTIgnoreOS: macos
// ----
// Warning 1218: (298-328): CHC: Error trying to invoke SMT solver.
// Warning 1218: (389-419): CHC: Error trying to invoke SMT solver.
// Warning 1218: (492-522): CHC: Error trying to invoke SMT solver.
// Warning 6328: (298-328): CHC: Assertion violation might happen here.
// Warning 6328: (389-419): CHC: Assertion violation might happen here.
// Warning 6328: (492-522): CHC: Assertion violation might happen here.
// Warning 4661: (298-328): BMC: Assertion violation happens here.
// Warning 4661: (389-419): BMC: Assertion violation happens here.
// Warning 4661: (492-522): BMC: Assertion violation happens here.
// Warning 6328: (298-328): CHC: Assertion violation happens here.\nCounterexample:\n\nt = false\nx = 0\ny = 0\nz = 0\nb4 = []\nb5 = []\n\nTransaction trace:\nC.constructor()\nC.abiEncodeSimple(false, 0, 0, 0, a, b)
// Warning 6328: (389-419): CHC: Assertion violation happens here.\nCounterexample:\n\nt = false\nx = 0\ny = 0\nz = 0\nb5 = []\n\nTransaction trace:\nC.constructor()\nC.abiEncodeSimple(false, 0, 0, 0, a, b)
// Warning 6328: (492-522): CHC: Assertion violation happens here.\nCounterexample:\n\nt = false\nx = 0\ny = 0\nz = 0\nb1 = []\nb2 = []\nb5 = []\n\nTransaction trace:\nC.constructor()\nC.abiEncodeSimple(false, 0, 0, 0, a, b)

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

@ -18,16 +18,9 @@ contract C {
}
// ====
// SMTEngine: all
// SMTIgnoreOS: macos
// ----
// Warning 1218: (208-238): CHC: Error trying to invoke SMT solver.
// Warning 1218: (286-316): CHC: Error trying to invoke SMT solver.
// Warning 1218: (453-483): CHC: Error trying to invoke SMT solver.
// Warning 1218: (532-562): CHC: Error trying to invoke SMT solver.
// Warning 6328: (208-238): CHC: Assertion violation might happen here.
// Warning 6328: (286-316): CHC: Assertion violation might happen here.
// Warning 6328: (453-483): CHC: Assertion violation might happen here.
// 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.
// Warning 6328: (208-238): CHC: Assertion violation happens here.\nCounterexample:\n\nb3 = []\nb4 = []\nb5 = []\n\nTransaction trace:\nC.constructor()\nC.abiEncodeStringLiteral()
// Warning 6328: (286-316): CHC: Assertion violation happens here.\nCounterexample:\n\nb2 = [0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d]\nb3 = [0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d]\nb4 = []\nb5 = []\n\nTransaction trace:\nC.constructor()\nC.abiEncodeStringLiteral()
// Warning 6328: (453-483): CHC: Assertion violation happens here.\nCounterexample:\n\nb5 = []\n\nTransaction trace:\nC.constructor()\nC.abiEncodeStringLiteral()
// Warning 6328: (532-562): CHC: Assertion violation happens here.\nCounterexample:\n\nb3 = [0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca]\n\nTransaction trace:\nC.constructor()\nC.abiEncodeStringLiteral()

11
test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_array_slice.sol
View File

@ -26,16 +26,7 @@ contract C {
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 1218: (578-608): CHC: Error trying to invoke SMT solver.
// Warning 1218: (691-721): CHC: Error trying to invoke SMT solver.
// Warning 1218: (959-989): CHC: Error trying to invoke SMT solver.
// Warning 1218: (1079-1109): CHC: Error trying to invoke SMT solver.
// Warning 6328: (325-355): CHC: Assertion violation happens here.
// Warning 6328: (578-608): CHC: Assertion violation might happen here.
// Warning 6328: (691-721): CHC: Assertion violation might happen here.
// Warning 6328: (959-989): CHC: Assertion violation might happen here.
// Warning 6328: (578-608): CHC: Assertion violation happens here.
// Warning 6328: (1079-1109): CHC: Assertion violation might happen here.
// Warning 4661: (578-608): BMC: Assertion violation happens here.
// Warning 4661: (691-721): BMC: Assertion violation happens here.
// Warning 4661: (959-989): BMC: Assertion violation happens here.
// Warning 4661: (1079-1109): BMC: Assertion violation happens here.

12
test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_array_slice_2.sol
View File

@ -24,17 +24,9 @@ contract C {
}
// ====
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 1218: (579-609): CHC: Error trying to invoke SMT solver.
// Warning 1218: (692-722): CHC: Error trying to invoke SMT solver.
// Warning 1218: (960-990): CHC: Error trying to invoke SMT solver.
// Warning 1218: (1080-1110): CHC: Error trying to invoke SMT solver.
// Warning 6328: (326-356): CHC: Assertion violation happens here.
// Warning 6328: (579-609): CHC: Assertion violation might happen here.
// Warning 6328: (692-722): CHC: Assertion violation might happen here.
// Warning 6328: (960-990): CHC: Assertion violation might happen here.
// Warning 6328: (579-609): CHC: Assertion violation happens here.
// Warning 6328: (1080-1110): CHC: Assertion violation might happen here.
// Warning 4661: (579-609): BMC: Assertion violation happens here.
// Warning 4661: (692-722): BMC: Assertion violation happens here.
// Warning 4661: (960-990): BMC: Assertion violation happens here.
// Warning 4661: (1080-1110): BMC: Assertion violation happens here.

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

@ -26,9 +26,7 @@ contract C {
// SMTIgnoreCex: yes
// ----
// Warning 5667: (100-115): Unused function parameter. Remove or comment out the variable name to silence this warning.
// Warning 1218: (855-885): CHC: Error trying to invoke SMT solver.
// Warning 6328: (571-601): CHC: Assertion violation happens here.
// Warning 6328: (691-721): CHC: Assertion violation happens here.
// Warning 6328: (740-770): CHC: Assertion violation happens here.
// Warning 6328: (855-885): CHC: Assertion violation might happen here.
// Warning 4661: (855-885): BMC: Assertion violation happens here.
// Warning 6328: (855-885): CHC: Assertion violation happens here.

21
test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_string_literal.sol
View File

@ -21,19 +21,10 @@ contract C {
}
// ====
// SMTEngine: all
// SMTIgnoreOS: macos
// ----
// Warning 1218: (252-282): CHC: Error trying to invoke SMT solver.
// Warning 1218: (347-377): CHC: Error trying to invoke SMT solver.
// Warning 1218: (531-561): CHC: Error trying to invoke SMT solver.
// Warning 1218: (627-657): CHC: Error trying to invoke SMT solver.
// Warning 1218: (746-776): CHC: Error trying to invoke SMT solver.
// Warning 6328: (252-282): CHC: Assertion violation might happen here.
// Warning 6328: (347-377): CHC: Assertion violation might happen here.
// Warning 6328: (531-561): CHC: Assertion violation might happen here.
// Warning 6328: (627-657): CHC: Assertion violation might happen here.
// Warning 6328: (746-776): CHC: Assertion violation might happen here.
// Warning 4661: (252-282): BMC: Assertion violation happens here.
// Warning 4661: (347-377): BMC: Assertion violation happens here.
// Warning 4661: (531-561): BMC: Assertion violation happens here.
// Warning 4661: (627-657): BMC: Assertion violation happens here.
// Warning 4661: (746-776): BMC: Assertion violation happens here.
// Warning 6328: (252-282): CHC: Assertion violation happens here.\nCounterexample:\n\nsel = 0x0\nb1 = [0x46, 0x46, 0x46, 0x46, 0x46, 0x46, 0x46, 0x46, 0x46, 0x46, 0x46, 0x46, 0x46, 0x46, 0x46, 0x46, 0x46, 0x46, 0x46]\nb3 = []\nb4 = []\nb5 = []\nb6 = []\n\nTransaction trace:\nC.constructor()\nC.abiEncodeStringLiteral(0x0)
// Warning 6328: (347-377): CHC: Assertion violation happens here.\nCounterexample:\n\nsel = 0x0\nb3 = [0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d]\nb4 = []\nb5 = []\nb6 = []\n\nTransaction trace:\nC.constructor()\nC.abiEncodeStringLiteral(0x0)
// Warning 6328: (531-561): CHC: Assertion violation happens here.\nCounterexample:\n\nsel = 0x0\nb1 = [0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90]\nb5 = []\nb6 = []\n\nTransaction trace:\nC.constructor()\nC.abiEncodeStringLiteral(0x0)
// Warning 6328: (627-657): CHC: Assertion violation happens here.\nCounterexample:\n\nsel = 0x0\nb5 = [0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1, 0xd1]\nb6 = []\n\nTransaction trace:\nC.constructor()\nC.abiEncodeStringLiteral(0x0)
// Warning 6328: (746-776): CHC: Assertion violation happens here.\nCounterexample:\n\nsel = 0x0\nb2 = []\nb5 = [0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2, 0xf2]\n\nTransaction trace:\nC.constructor()\nC.abiEncodeStringLiteral(0x0)

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

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

12
test/libsolidity/smtCheckerTests/abi/abi_encode_with_sig_array_slice.sol
View File

@ -24,17 +24,9 @@ contract C {
}
// ====
// SMTEngine: all
// SMTIgnoreOS: macos
// ----
// Warning 1218: (588-618): CHC: Error trying to invoke SMT solver.
// Warning 1218: (702-732): CHC: Error trying to invoke SMT solver.
// Warning 1218: (971-1001): CHC: Error trying to invoke SMT solver.
// Warning 1218: (1086-1116): CHC: Error trying to invoke SMT solver.
// Warning 6328: (334-364): CHC: Assertion violation happens here.
// Warning 6328: (588-618): CHC: Assertion violation might happen here.
// Warning 6328: (702-732): CHC: Assertion violation might happen here.
// Warning 6328: (971-1001): CHC: Assertion violation might happen here.
// Warning 6328: (588-618): CHC: Assertion violation happens here.
// Warning 6328: (1086-1116): CHC: Assertion violation might happen here.
// Warning 4661: (588-618): BMC: Assertion violation happens here.
// Warning 4661: (702-732): BMC: Assertion violation happens here.
// Warning 4661: (971-1001): BMC: Assertion violation happens here.
// Warning 4661: (1086-1116): BMC: Assertion violation happens here.

14
test/libsolidity/smtCheckerTests/abi/abi_encode_with_sig_array_slice_2.sol
View File

@ -24,17 +24,9 @@ contract C {
}
// ====
// SMTEngine: all
// SMTIgnoreOS: macos
// ----
// Warning 1218: (589-619): CHC: Error trying to invoke SMT solver.
// Warning 1218: (703-733): CHC: Error trying to invoke SMT solver.
// Warning 1218: (972-1002): CHC: Error trying to invoke SMT solver.
// Warning 1218: (1087-1117): CHC: Error trying to invoke SMT solver.
// Warning 6328: (335-365): CHC: Assertion violation happens here.
// Warning 6328: (589-619): CHC: Assertion violation might happen here.
// Warning 6328: (703-733): CHC: Assertion violation might happen here.
// Warning 6328: (972-1002): CHC: Assertion violation might happen here.
// Warning 6328: (335-365): CHC: Assertion violation happens here.\nCounterexample:\n\ndata = [69]\nb2 = [0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43, 0x43]\nb3 = []\nb4 = []\nx = 0\ny = 0\nb5 = []\nb6 = []\n\nTransaction trace:\nC.constructor()\nC.abiEncodeSlice(sig, [69])
// Warning 6328: (589-619): CHC: Assertion violation happens here.
// Warning 6328: (1087-1117): CHC: Assertion violation might happen here.
// Warning 4661: (589-619): BMC: Assertion violation happens here.
// Warning 4661: (703-733): BMC: Assertion violation happens here.
// Warning 4661: (972-1002): BMC: Assertion violation happens here.
// Warning 4661: (1087-1117): BMC: Assertion violation happens here.

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

@ -12,6 +12,7 @@ contract C {
}
// ====
// SMTEngine: all
// SMTIgnoreOS: macos
// ----
// Warning 6328: (337-375): CHC: Assertion violation happens here.
// Warning 6328: (394-432): CHC: Assertion violation happens here.
// Warning 6328: (337-375): CHC: Assertion violation happens here.\nCounterexample:\n\na = 0\nb = 0\nb1 = [0x1d, 0x1d, 0x1d, 0x1d, 0x1d, 0x1d, 0x1d, 0x1d, 0x1d, 0x1d, 0x1d, 0x1d, 0x1d, 0x1d, 0x1d, 0x1d, 0x1d, 0x1d, 0x1d]\nb2 = [0x1d, 0x1d, 0x1d, 0x1d, 0x1d, 0x1d, 0x1d, 0x1d, 0x1d, 0x1d, 0x1d, 0x1d, 0x1d, 0x1d, 0x1d, 0x1d, 0x1d, 0x1d, 0x1d]\n\nTransaction trace:\nC.constructor()\nC.abiEncodeHash(sig, 0, 0)
// Warning 6328: (394-432): CHC: Assertion violation happens here.\nCounterexample:\n\na = 0\nb = 0\n\nTransaction trace:\nC.constructor()\nC.abiEncodeHash(sig, 0, 0)

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

@ -22,11 +22,10 @@ contract C {
}
// ====
// SMTEngine: all
// SMTIgnoreOS: macos
// ----
// 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.\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.
// Warning 4661: (824-854): BMC: Assertion violation happens here.
// Warning 6328: (664-694): CHC: Assertion violation happens here.\nCounterexample:\n\nt = false\nx = 0\ny = 0\nz = 0\nb6 = []\n\nTransaction trace:\nC.constructor()\nC.abiEncodeSimple(sig, false, 0, 0, 0, a, b)
// Warning 6328: (713-743): CHC: Assertion violation happens here.\nCounterexample:\n\nt = false\nx = 0\ny = 0\nz = 0\nb6 = []\n\nTransaction trace:\nC.constructor()\nC.abiEncodeSimple(sig, false, 0, 0, 0, a, b)
// Warning 6328: (824-854): CHC: Assertion violation happens here.

21
test/libsolidity/smtCheckerTests/abi/abi_encode_with_sig_string_literal.sol
View File

@ -21,19 +21,10 @@ contract C {
}
// ====
// SMTEngine: all
// SMTIgnoreOS: macos
// ----
// Warning 1218: (261-291): CHC: Error trying to invoke SMT solver.
// Warning 1218: (357-387): CHC: Error trying to invoke SMT solver.
// Warning 1218: (542-572): CHC: Error trying to invoke SMT solver.
// Warning 1218: (639-669): CHC: Error trying to invoke SMT solver.
// Warning 1218: (753-783): CHC: Error trying to invoke SMT solver.
// Warning 6328: (261-291): CHC: Assertion violation might happen here.
// Warning 6328: (357-387): CHC: Assertion violation might happen here.
// Warning 6328: (542-572): CHC: Assertion violation might happen here.
// Warning 6328: (639-669): CHC: Assertion violation might happen here.
// Warning 6328: (753-783): CHC: Assertion violation might happen here.
// Warning 4661: (261-291): BMC: Assertion violation happens here.
// Warning 4661: (357-387): BMC: Assertion violation happens here.
// Warning 4661: (542-572): BMC: Assertion violation happens here.
// Warning 4661: (639-669): BMC: Assertion violation happens here.
// Warning 4661: (753-783): BMC: Assertion violation happens here.
// Warning 6328: (261-291): CHC: Assertion violation happens here.\nCounterexample:\n\nb2 = [0x5a, 0x5a, 0x5a, 0x5a, 0x5a, 0x5a, 0x5a, 0x5a, 0x5a, 0x5a, 0x5a, 0x5a, 0x5a, 0x5a, 0x5a, 0x5a, 0x5a, 0x5a, 0x5a, 0x5a, 0x5a, 0x5a, 0x5a, 0x5a, 0x5a, 0x5a, 0x5a, 0x5a, 0x5a, 0x5a, 0x5a, 0x5a, 0x5a, 0x5a, 0x5a, 0x5a, 0x5a, 0x5a, 0x5a, 0x5a, 0x5a, 0x5a, 0x5a, 0x5a, 0x5a, 0x5a, 0x5a, 0x5a, 0x5a, 0x5a, 0x5a, 0x5a, 0x5a, 0x5a, 0x5a, 0x5a, 0x5a, 0x5a, 0x5a, 0x5a, 0x5a, 0x5a, 0x5a, 0x5a, 0x5a, 0x5a]\nb3 = []\nb4 = []\nb5 = []\nb6 = []\n\nTransaction trace:\nC.constructor()\nC.abiEncodeStringLiteral(sig)
// Warning 6328: (357-387): CHC: Assertion violation happens here.\nCounterexample:\n\nb3 = [0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90, 0x90]\nb4 = []\nb5 = []\nb6 = []\n\nTransaction trace:\nC.constructor()\nC.abiEncodeStringLiteral(sig)
// Warning 6328: (542-572): CHC: Assertion violation happens here.\nCounterexample:\n\nb3 = [0xaa, 0xaa, 0xaa, 0xaa, 0xaa, 0xaa, 0xaa, 0xaa, 0xaa, 0xaa, 0xaa, 0xaa, 0xaa, 0xaa, 0xaa, 0xaa, 0xaa, 0xaa, 0xaa, 0xaa, 0xaa, 0xaa, 0xaa, 0xaa, 0xaa, 0xaa, 0xaa, 0xaa, 0xaa, 0xaa, 0xaa, 0xaa, 0xaa, 0xaa, 0xaa, 0xaa, 0xaa, 0xaa, 0xaa, 0xaa, 0xaa, 0xaa, 0xaa, 0xaa, 0xaa, 0xaa, 0xaa, 0xaa, 0xaa, 0xaa, 0xaa, 0xaa, 0xaa, 0xaa, 0xaa, 0xaa, 0xaa, 0xaa, 0xaa, 0xaa, 0xaa, 0xaa, 0xaa, 0xaa, 0xaa, 0xaa]\nb5 = []\nb6 = []\n\nTransaction trace:\nC.constructor()\nC.abiEncodeStringLiteral(sig)
// Warning 6328: (639-669): CHC: Assertion violation happens here.\nCounterexample:\n\nb4 = [0x22, 0x22, 0x22, 0x22, 0x22, 0x0d, 0x22, 0x22, 0x22, 0x22, 0x09, 0x22, 0x0b, 0x22, 0x22, 0x0e, 0x22, 0x10, 0x22, 0x12, 0x22, 0x14, 0x22, 0x16, 0x22, 0x18, 0x22, 0x1a, 0x22, 0x1c, 0x22, 0x1e, 0x22, 0x20, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22, 0x22]\nb6 = []\n\nTransaction trace:\nC.constructor()\nC.abiEncodeStringLiteral(sig)
// Warning 6328: (753-783): CHC: Assertion violation happens here.\nCounterexample:\n\nb2 = [0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117]\nb4 = []\nb5 = [0x0118, 0x0118, 0x0118, 0x0118, 0x0118, 0x0118, 0x0118, 0x0118, 0x0118, 0x0118, 0x0118, 0x0118, 0x0118, 0x0118, 0x0118, 0x0118, 0x0118, 0x0118, 0x0118, 0x0118, 0x0118, 0x0118, 0x0118, 0x0118, 0x0118, 0x0118, 0x0118, 0x0118, 0x0118, 0x0118, 0x0118, 0x0118, 0x0118, 0x0118, 0x0118, 0x0118, 0x0118, 0x0118, 0x0118, 0x0118, 0x0118, 0x0118, 0x0118, 0x0118, 0x0118, 0x0118, 0x0118, 0x0118, 0x0118, 0x0118, 0x0118, 0x0118, 0x0118, 0x0118, 0x0118, 0x0118, 0x0118, 0x0118, 0x0118, 0x0118, 0x0118, 0x0118, 0x0118, 0x0118, 0x0118, 0x0118]\n\nTransaction trace:\nC.constructor()\nC.abiEncodeStringLiteral(sig)

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

@ -19,4 +19,4 @@ contract C {
// SMTEngine: all
// SMTIgnoreOS: macos
// ----
// Warning 6328: (199-229): CHC: Assertion violation happens here.
// Warning 6328: (199-229): CHC: Assertion violation happens here.\nCounterexample:\nb = [1]\n\nTransaction trace:\nC.constructor()\nState: b = []\nC.g()

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

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

1
test/libsolidity/smtCheckerTests/array_members/push_storage_ref_unsafe_length.sol
View File

@ -25,6 +25,7 @@ contract C {
}
// ====
// SMTEngine: all
// SMTIgnoreOS: macos
// ----
// Warning 6368: (238-242): CHC: Out of bounds access happens here.
// Warning 6368: (238-245): CHC: Out of bounds access might happen here.

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

@ -14,7 +14,4 @@ contract C {
// SMTEngine: all
// SMTIgnoreOS: macos
// ----
// Warning 1218: (131-165): CHC: Error trying to invoke SMT solver.
// Warning 6328: (131-165): CHC: Assertion violation might happen here.
// Info 1180: Reentrancy property(ies) for :C:\n(!(<errorCode> >= 2) && (((:var 0).balances[address(this)] + ((- 1) * (:var 1).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
// Warning 4661: (131-165): BMC: Assertion violation happens here.
// Warning 6328: (131-165): CHC: Assertion violation happens here.\nCounterexample:\n\n_i = 0\nx = 282\n\nTransaction trace:\nC.constructor()\nC.f(0)\n _i.ext() -- untrusted external call, synthesized as:\n C.f(0) -- reentrant call\n _i.ext() -- untrusted external call

4
test/libsolidity/smtCheckerTests/control_flow/branches_inside_modifiers_2.sol
View File

@ -21,6 +21,6 @@ contract C {
}
// ====
// SMTEngine: all
// SMTIgnoreOS: macos
// ----
// Warning 6328: (333-347): CHC: Assertion violation happens here.\nCounterexample:\nx = 3\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.g()\n C.f() -- internal call
// Info 1180: Contract invariant(s) for :C:\n((x = 0) || (x = 3))\n
// Warning 6328: (333-347): CHC: Assertion violation happens here.

12
test/libsolidity/smtCheckerTests/crypto/crypto_functions_compare_hashes.sol
View File

@ -12,12 +12,6 @@ contract C {
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 1218: (150-164): CHC: Error trying to invoke SMT solver.
// Warning 1218: (168-182): CHC: Error trying to invoke SMT solver.
// Warning 1218: (186-200): CHC: Error trying to invoke SMT solver.
// Warning 6328: (150-164): CHC: Assertion violation might happen here.
// Warning 6328: (168-182): CHC: Assertion violation might happen here.
// Warning 6328: (186-200): CHC: Assertion violation might happen here.
// Warning 4661: (150-164): BMC: Assertion violation happens here.
// Warning 4661: (168-182): BMC: Assertion violation happens here.
// Warning 4661: (186-200): BMC: Assertion violation happens here.
// Warning 6328: (150-164): CHC: Assertion violation happens here.
// Warning 6328: (168-182): CHC: Assertion violation happens here.
// Warning 6328: (186-200): CHC: Assertion violation happens here.

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

@ -33,6 +33,4 @@ contract C {
// Warning 2072: (435-445): Unused local variable.
// Warning 2072: (656-666): Unused local variable.
// Warning 2072: (698-708): 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 4661: (135-151): BMC: Assertion violation happens here.
// Warning 6328: (135-151): CHC: Assertion violation happens here.

4
test/libsolidity/smtCheckerTests/crypto/crypto_functions_not_same.sol
View File

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

12
test/libsolidity/smtCheckerTests/crypto/crypto_functions_same_input_over_state_same_output.sol
View File

@ -37,15 +37,3 @@ contract C {
// ====
// SMTEngine: all
// ----
// Warning 1218: (544-563): CHC: Error trying to invoke SMT solver.
// Warning 1218: (567-586): CHC: Error trying to invoke SMT solver.
// Warning 1218: (590-609): CHC: Error trying to invoke SMT solver.
// Warning 1218: (613-632): CHC: Error trying to invoke SMT solver.
// Warning 6328: (544-563): CHC: Assertion violation might happen here.
// Warning 6328: (567-586): CHC: Assertion violation might happen here.
// Warning 6328: (590-609): CHC: Assertion violation might happen here.
// Warning 6328: (613-632): CHC: Assertion violation might happen here.
// Warning 4661: (544-563): BMC: Assertion violation happens here.
// Warning 4661: (567-586): BMC: Assertion violation happens here.
// Warning 4661: (590-609): BMC: Assertion violation happens here.
// Warning 4661: (613-632): BMC: Assertion violation happens here.

13
test/libsolidity/smtCheckerTests/crypto/crypto_functions_same_input_over_state_same_output_fail.sol
View File

File diff suppressed because one or more lines are too long

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

@ -21,4 +21,4 @@ contract C {
// 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 = 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()

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

@ -44,7 +44,5 @@ 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 might happen here.
// Warning 4661: (437-463): BMC: Assertion violation happens here.
// Warning 6328: (437-463): CHC: Assertion violation happens here.

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

@ -17,6 +17,4 @@ 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.
// Warning 4661: (206-220): BMC: Assertion violation happens here.
// Warning 6328: (206-220): 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.broken() -- reentrant call

8
test/libsolidity/smtCheckerTests/external_calls/external_reentrancy_crypto.sol
View File

@ -26,10 +26,6 @@ contract C {
// ====
// SMTEngine: all
// SMTIgnoreInv: yes
// SMTIgnoreCex: yes
// ----
// Warning 1218: (264-283): CHC: Error trying to invoke SMT solver.
// Warning 1218: (302-333): CHC: Error trying to invoke SMT solver.
// Warning 6328: (264-283): CHC: Assertion violation might happen here.
// Warning 6328: (302-333): CHC: Assertion violation might happen here.
// Warning 4661: (264-283): BMC: Assertion violation happens here.
// Warning 4661: (302-333): BMC: Assertion violation happens here.
// Warning 6328: (302-333): CHC: Assertion violation happens here.

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

@ -26,4 +26,4 @@ contract C {
}
}
// ----
// Warning 6328: (337-351): CHC: Assertion violation happens here.\nCounterexample:\nx = 2, inG = true\n_i = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0, inG = false\nC.g(0)\n L.g(0) -- internal call\n L.f(0) -- internal call\n _i.i() -- untrusted external call, synthesized as:\n C.s() -- reentrant call
// Warning 6328: (337-351): CHC: Assertion violation happens here.

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

@ -29,4 +29,4 @@ contract C {
}
}
// ----
// Warning 6328: (354-368): CHC: Assertion violation happens here.\nCounterexample:\nx = 2, inG = true\n_i = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0, inG = false\nC.g(0)\n L.g(0) -- internal call\n M.f(0) -- internal call\n _i.i() -- untrusted external call, synthesized as:\n C.s() -- reentrant call
// Warning 6328: (354-368): CHC: Assertion violation happens here.

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.supportsInterface(0x01ffc9a7)\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.check()\n Homer.supportsInterface(0x73b6b492) -- internal call\n Homer.supportsInterface(0x01ffc9a7) -- internal call\n Homer.supportsInterface(0x8b9eb9ca) -- internal call

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.\nCounterexample:\nstr2 = [0x63]\na2 = [0x63]\n\nTransaction trace:\nC.constructor()\nState: str2 = [0x63]\nC.f()

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.\nCounterexample:\nstr1 = [0x62]\na1 = [0x62]\n\nTransaction trace:\nC.constructor()\nState: str1 = [0x62]\nC.f()

10
test/libsolidity/smtCheckerTests/functions/getters/struct_3.sol
View File

@ -21,12 +21,4 @@ contract C {
// ====
// SMTEngine: all
// ----
// Warning 1218: (273-277): CHC: Error trying to invoke SMT solver.
// Warning 1218: (281-287): CHC: Error trying to invoke SMT solver.
// Warning 1218: (314-318): CHC: Error trying to invoke SMT solver.
// Warning 1218: (307-326): CHC: Error trying to invoke SMT solver.
// Warning 6368: (273-277): CHC: Out of bounds access might happen here.
// Warning 6368: (281-287): CHC: Out of bounds access might happen here.
// Warning 6368: (314-318): CHC: Out of bounds access might happen here.
// Warning 6328: (307-326): CHC: Assertion violation might happen here.
// Warning 4661: (307-326): BMC: Assertion violation happens here.
// Warning 6328: (307-326): CHC: Assertion violation happens here.

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

@ -23,5 +23,6 @@ contract C {
}
// ====
// SMTEngine: all
// SMTIgnoreOS: macos
// ----
// Warning 6328: (261-283): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.g2(){ msg.value: 1 }\n C.i() -- internal call
// Warning 6328: (261-283): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.g2(){ msg.value: 3529 }\n C.i() -- internal call

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

@ -18,9 +18,5 @@ function f(uint _x) pure {
// ====
// SMTEngine: all
// ----
// 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.
// 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

1
test/libsolidity/smtCheckerTests/invariants/state_machine_1.sol
View File

@ -31,5 +31,6 @@ contract C {
// ====
// SMTEngine: all
// SMTSolvers: z3
// SMTIgnoreOS: macos
// ----
// Info 1180: Contract invariant(s) for :C:\n!(x >= 7)\n

1
test/libsolidity/smtCheckerTests/loops/for_loop_array_assignment_memory_storage.sol
View File

@ -25,4 +25,5 @@ contract LoopFor2 {
// ====
// SMTEngine: all
// SMTSolvers: z3
// SMTIgnoreOS: macos
// ----

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

@ -19,7 +19,6 @@ contract C {
}
// ====
// SMTEngine: all
// SMTIgnoreOS: macos
// ----
// 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.
// 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.f()\nState: x = 0, owner = 0x0\nC.g(1)\n C.f() -- internal call

2
test/libsolidity/smtCheckerTests/modifiers/modifier_parameter_copy.sol
View File

@ -12,4 +12,4 @@ contract C
// ====
// SMTEngine: all
// ----
// Warning 6328: (95-109): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 3\nx = 3\n\nTransaction trace:\nC.constructor()\nC.f(3)
// Warning 6328: (95-109): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 0\nx = 0\n\nTransaction trace:\nC.constructor()\nC.f(0)

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.
// Warning 6328: (162-181): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 2\np = 0\n\nTransaction trace:\nC.constructor()\nC.f(2, 0)

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

@ -16,6 +16,7 @@ contract C {
}
// ====
// SMTEngine: all
// SMTIgnoreOS: macos
// ----
// 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 happens here.\nCounterexample:\n\ny = 0x63666566676e616263666566676e616263666566676e616263666566676e6162\nz = 0x63666566676e616263666566676e616263666566676e616263666566676e6162\n\nTransaction trace:\nC.constructor()\nC.f()

1
test/libsolidity/smtCheckerTests/operators/compound_mul_array_index.sol
View File

@ -13,5 +13,6 @@ contract C
}
// ====
// SMTEngine: all
// SMTIgnoreOS: macos
// ----
// Warning 6328: (226-247): CHC: Assertion violation happens here.\nCounterexample:\narray = [100]\nx = 0\np = 0\n\nTransaction trace:\nC.constructor()\nState: array = []\nC.q()\nState: array = [0]\nC.f(0, 0)

9
test/libsolidity/smtCheckerTests/out_of_bounds/array_2d_4.sol
View File

@ -14,15 +14,12 @@ contract C {
// ====
// SMTEngine: all
// ----
// Warning 1218: (228-232): CHC: Error trying to invoke SMT solver.
// Warning 1218: (255-259): CHC: Error trying to invoke SMT solver.
// Warning 1218: (255-262): CHC: Error trying to invoke SMT solver.
// Warning 4984: (184-197): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
// Warning 4984: (199-202): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
// Warning 6368: (228-232): CHC: Out of bounds access might happen here.
// Warning 6368: (228-232): CHC: Out of bounds access happens here.\nCounterexample:\na = []\ni = 0\nj = 0\n\nTransaction trace:\nC.constructor()\nState: a = []\nC.r()
// Warning 4984: (228-244): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
// Warning 4984: (246-249): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
// Warning 6368: (255-259): CHC: Out of bounds access might happen here.
// Warning 6368: (255-262): CHC: Out of bounds access might happen here.
// Warning 6368: (255-259): CHC: Out of bounds access happens here.\nCounterexample:\na = []\ni = 0\nj = 0\n\nTransaction trace:\nC.constructor()\nState: a = []\nC.r()
// Warning 6368: (255-262): CHC: Out of bounds access happens here.
// Warning 2661: (184-197): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 2661: (228-244): BMC: Overflow (resulting value larger than 2**256 - 1) 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 2**255 - 1) happens here.\nCounterexample:\n\nx = 57896044618658097711785492504343953926634992332820282019728792003956564819967\ny = (- 1)\n = 0\n\nTransaction trace:\nC.constructor()\nC.f(57896044618658097711785492504343953926634992332820282019728792003956564819967, (- 1))
// Warning 4984: (96-101): CHC: Overflow (resulting value larger than 2**255 - 1) happens here.\nCounterexample:\n\nx = 0\ny = (- 57896044618658097711785492504343953926634992332820282019728792003956564819968)\n = 0\n\nTransaction trace:\nC.constructor()\nC.f(0, (- 57896044618658097711785492504343953926634992332820282019728792003956564819968))

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

@ -13,4 +13,4 @@ contract C {
// Warning 2072: (82-86): Unused local variable.
// Warning 2072: (140-150): Unused local variable.
// Warning 2072: (152-156): Unused local variable.
// Warning 6328: (220-236): CHC: Assertion violation happens here.
// Warning 6328: (220-236): CHC: Assertion violation happens here.\nCounterexample:\n\na1 = 2437\nb1 = 0x0b\nc1 = 10\na2 = 2437\nb2 = 0x0b\nc2 = 10\n\nTransaction trace:\nC.constructor()\nC.f(data)

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

@ -21,4 +21,4 @@ contract C {
// SMTEngine: chc
// SMTIgnoreOS: macos
// ----
// Warning 6328: (343-377): CHC: Assertion violation happens here.\nCounterexample:\ngas = 0, origin = 0x52f7\n\nTransaction trace:\nC.constructor()\nState: gas = 0, origin = 0x0\nC.f(){ tx.gasprice: 0, tx.origin: 0x52f7 }\n C.g() -- internal call
// Warning 6328: (343-377): CHC: Assertion violation happens here.\nCounterexample:\ngas = 0, origin = 0x0\n\nTransaction trace:\nC.constructor()\nState: gas = 0, origin = 0x0\nC.f(){ tx.gasprice: 0, tx.origin: 0x0 }\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 = 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
// Warning 6328: (135-169): CHC: Assertion violation happens here.\nCounterexample:\n\n_i = 0\nx = 5892\n\nTransaction trace:\nC.constructor()\nC.g(0){ msg.value: 11 }\n _i.f() -- untrusted external call, synthesized as:\n C.g(0){ msg.value: 32278 } -- reentrant call\n _i.f() -- untrusted external call

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

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

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:\n\n\nTransaction trace:\nC.constructor()\nState: x = []\nC.s()
// Warning 6328: (132-160): CHC: Assertion violation happens here.\nCounterexample:\nx = [0x61, 0x62, 0x63, 0x61]\n\nTransaction trace:\nC.constructor()\nState: x = []\nC.s()

2
test/libsolidity/smtCheckerTests/types/abi_type_type_1.sol
View File

@ -7,4 +7,4 @@ contract C {
// ====
// SMTEngine: all
// ----
// Warning 6328: (107-128): CHC: Assertion violation happens here.
// Warning 6328: (107-128): CHC: Assertion violation happens here.\nCounterexample:\n\na = false\nx = 2\n\nTransaction trace:\nC.constructor()\nC.f(d)

10
test/libsolidity/smtCheckerTests/types/array_aliasing_storage_3.sol
View File

@ -35,11 +35,7 @@ contract C
// SMTIgnoreCex: yes
// ----
// Warning 2072: (384-399): Unused local variable.
// Warning 1218: (955-959): CHC: Error trying to invoke SMT solver.
// Warning 1218: (948-965): CHC: Error trying to invoke SMT solver.
// Warning 1218: (976-980): CHC: Error trying to invoke SMT solver.
// Warning 6368: (489-493): CHC: Out of bounds access happens here.
// Warning 6368: (955-959): CHC: Out of bounds access might happen here.
// Warning 6328: (948-965): CHC: Assertion violation might happen here.
// Warning 6368: (976-980): CHC: Out of bounds access might happen here.
// Warning 4661: (948-965): BMC: Assertion violation happens here.
// Warning 6368: (955-959): CHC: Out of bounds access happens here.
// Warning 6328: (948-965): CHC: Assertion violation happens here.
// Warning 6368: (976-980): CHC: Out of bounds access happens here.

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

@ -12,6 +12,4 @@ contract C
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// 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.
// Warning 6328: (143-159): CHC: Assertion violation happens here.

2
test/libsolidity/smtCheckerTests/types/array_static_aliasing_memory_5.sol
View File

@ -16,4 +16,4 @@ contract C
// ====
// SMTEngine: all
// ----
// Warning 6328: (385-402): CHC: Assertion violation happens here.
// Warning 6328: (385-402): CHC: Assertion violation happens here.\nCounterexample:\n\na = [2440, 11]\nb = [1, 8]\nc = [15, 15]\n\nTransaction trace:\nC.constructor()\nC.f([2, 13], [0, 8], [42, 12])

2
test/libsolidity/smtCheckerTests/types/bool_simple_2.sol
View File

@ -6,4 +6,4 @@ contract C {
// ====
// SMTEngine: all
// ----
// Warning 6328: (66-80): CHC: Assertion violation happens here.\nCounterexample:\n\nx = false\ny = true\n\nTransaction trace:\nC.constructor()\nC.f(false, true)
// Warning 6328: (66-80): CHC: Assertion violation happens here.\nCounterexample:\n\nx = true\ny = false\n\nTransaction trace:\nC.constructor()\nC.f(true, false)

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

@ -53,4 +53,3 @@ contract C {
// ====
// SMTEngine: all
// ----
// Warning 6368: (212-217): CHC: Out of bounds access might happen 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_array_branches_2d.sol
View File

@ -15,6 +15,6 @@ contract C
}
// ====
// SMTEngine: all
// SMTIgnoreOS: macos
// ----
// Warning 6368: (216-225): CHC: Out of bounds access might happen here.
// Warning 6328: (209-230): CHC: Assertion violation might happen here.

2
test/libsolidity/smtCheckerTests/userTypes/user_abi_1.sol
View File

@ -11,4 +11,4 @@ contract C {
// ====
// SMTEngine: all
// ----
// Warning 6328: (188-212): CHC: Assertion violation happens here.
// Warning 6328: (188-212): CHC: Assertion violation happens here.\nCounterexample:\n\ny = 2437\n\nTransaction trace:\nC.constructor()\nC.f(data)

2
test/libsolidity/smtCheckerTests/userTypes/user_abi_2.sol
View File

@ -11,4 +11,4 @@ contract C {
// ====
// SMTEngine: all
// ----
// Warning 6328: (192-226): CHC: Assertion violation happens here.
// Warning 6328: (192-226): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f(data)