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 #13016 from ethereum/z3_17

Browse Source 
Update tests and hashes for z3 4.8.17
This commit is contained in:
Daniel Kirchner 2022-05-13 17:46:03 +02:00 committed by GitHub
commit e1972da29a
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
7 changed files with 18 additions and 17 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-12
default: "solbuildpackpusher/solidity-buildpack-deps@sha256:43675fb5225df7cebffbe10d26e37099ed70a8398ff348c3512c2a698e435a36"
# solbuildpackpusher/solidity-buildpack-deps:ubuntu2004-13
default: "solbuildpackpusher/solidity-buildpack-deps@sha256:aa64242ecba4f040a839eadfaf20e8489cf93d1cb96ab90df2b240cdbbfe7f7c"
ubuntu-2004-clang-docker-image:
type: string
# solbuildpackpusher/solidity-buildpack-deps:ubuntu2004.clang-12
default: "solbuildpackpusher/solidity-buildpack-deps@sha256:39a628620c35d61033b11f033dbcca342cbacc0e51fd190e06f7db1e74470197"
# solbuildpackpusher/solidity-buildpack-deps:ubuntu2004.clang-13
default: "solbuildpackpusher/solidity-buildpack-deps@sha256:caaf8d42aaf07397d1540e570f096a4fb1ef11fda7da3f1141d8852ec8322a9e"
ubuntu-1604-clang-ossfuzz-docker-image:
type: string
# solbuildpackpusher/solidity-buildpack-deps:ubuntu1604.clang.ossfuzz-17
default: "solbuildpackpusher/solidity-buildpack-deps@sha256:fd67ac47de58b0eff088c72ae1f6261b27df3d89b1f67ad3ed9c40fee8471228"
# solbuildpackpusher/solidity-buildpack-deps:ubuntu1604.clang.ossfuzz-18
default: "solbuildpackpusher/solidity-buildpack-deps@sha256:048002d71a1f86f83dedb79dd057760b752256c75646ba5ad5c1bbe92e1695aa"
emscripten-docker-image:
type: string
# solbuildpackpusher/solidity-buildpack-deps:emscripten-10
default: "solbuildpackpusher/solidity-buildpack-deps@sha256:feac0e5fba12c346ad18d70eb10e98ffabba80da25074a71b22dced4f2148aed"
# solbuildpackpusher/solidity-buildpack-deps:emscripten-11
default: "solbuildpackpusher/solidity-buildpack-deps@sha256:0ad7c65e8c54d926ba9cb80d56246e4fc49f9284ad5188aaaa4834f46ab0c315"
evm-version:
type: string
default: london

4
.circleci/osx_install_dependencies.sh
View File

@ -61,11 +61,11 @@ then
./scripts/install_obsolete_jsoncpp_1_7_4.sh
# z3
z3_version="4.8.16"
z3_version="4.8.17"
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" 71ed7b6d10c01198187df72cccb8eb6de6d9aa2bf9557b3dd052032524b598a5
validate_checksum "$z3_package" 189667930517aee07f1ce36485d5924a9a2cb4f8c3c9586b03e714a2c657541a
unzip "$z3_package"
rm "$z3_package"
cp "${z3_dir}/bin/libz3.a" /usr/local/lib

2
CMakeLists.txt
View File

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

4
scripts/build_emscripten.sh
View File

@ -34,7 +34,7 @@ else
BUILD_DIR="$1"
fi
# solbuildpackpusher/solidity-buildpack-deps:emscripten-10
# solbuildpackpusher/solidity-buildpack-deps:emscripten-11
docker run -v "$(pwd):/root/project" -w /root/project \
solbuildpackpusher/solidity-buildpack-deps@sha256:feac0e5fba12c346ad18d70eb10e98ffabba80da25074a71b22dced4f2148aed \
solbuildpackpusher/solidity-buildpack-deps@sha256:0ad7c65e8c54d926ba9cb80d56246e4fc49f9284ad5188aaaa4834f46ab0c315 \
./scripts/ci/build_emscripten.sh "$BUILD_DIR"

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

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

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

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

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

@ -21,5 +21,4 @@ contract C {
// SMTEngine: all
// SMTIgnoreOS: macos
// ----
// Warning 6328: (280-300): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f()
// Info 1180: Contract invariant(s) for :C:\n!(m[0].length <= 1)\n(!(m[0][1] >= 43) && !(m[0][1] <= 41))\n
// Warning 6328: (280-300): CHC: Assertion violation happens here.