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 #9797 from ethereum/smt_z3_update

Browse Source 
Update SMTChecker tests with z3 4.8.9
This commit is contained in:
Daniel Kirchner 2020-09-14 20:02:10 +02:00 committed by GitHub
commit 857a48f526
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
8 changed files with 20 additions and 21 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

18
.circleci/config.yml
View File

@ -9,23 +9,23 @@ version: 2.1
parameters:
ubuntu-1804-docker-image:
type: string
# solbuildpackpusher/solidity-buildpack-deps:ubuntu1804-2
default: "solbuildpackpusher/solidity-buildpack-deps@sha256:9ab317e583c395e50884ba82e9f99811c374344cea4c550725be8ec836e07acc"
# solbuildpackpusher/solidity-buildpack-deps:ubuntu1804-3
default: "solbuildpackpusher/solidity-buildpack-deps@sha256:19f613d2ac47fedff654dacef984d8a64726c4d67ae8f2667a85ee7d97ac4c1c"
ubuntu-2004-docker-image:
type: string
# solbuildpackpusher/solidity-buildpack-deps:ubuntu2004-2
default: "solbuildpackpusher/solidity-buildpack-deps@sha256:cbfa42d8ecbe94391ba8837e218869242666de7a0da6ccac065a856c85b6a6a0"
# solbuildpackpusher/solidity-buildpack-deps:ubuntu2004-3
default: "solbuildpackpusher/solidity-buildpack-deps@sha256:aeedbe7390a7383815f0cf0f8a1b8bf84dc5e334a3b0043ebcdf8b1bdbe80a81"
ubuntu-2004-clang-docker-image:
type: string
# solbuildpackpusher/solidity-buildpack-deps:ubuntu2004.clang-2
default: "solbuildpackpusher/solidity-buildpack-deps@sha256:7a4d5271b5552139d9f2caefc50d42f401bf74132cf8f253e199e11c80ab42de"
# solbuildpackpusher/solidity-buildpack-deps:ubuntu2004.clang-3
default: "solbuildpackpusher/solidity-buildpack-deps@sha256:2593c15689dee5b5bdfff96a36c8c68a468cd3b147c41f75b820b8fabc257be9"
ubuntu-1604-clang-ossfuzz-docker-image:
type: string
# solbuildpackpusher/solidity-buildpack-deps:ubuntu1604.clang.ossfuzz-3
default: "solbuildpackpusher/solidity-buildpack-deps@sha256:6fa6914bd81abcac4b162c738e6ff05d87cefe7655e3859c7a827e5a8ec20dc7"
# solbuildpackpusher/solidity-buildpack-deps:ubuntu1604.clang.ossfuzz-4
default: "solbuildpackpusher/solidity-buildpack-deps@sha256:842126b164b3542f05bff2611459e21edc7e3e2c81ca9d1f43396c8cf066f7ca"
emscripten-docker-image:
type: string
default: "solbuildpackpusher/solidity-buildpack-deps@sha256:d557d015918c3cf68b0d22839bab41013f0757b651a7fef21595f89721dbebcc"
default: "solbuildpackpusher/solidity-buildpack-deps@sha256:23dad3b34deae8107c8551804ef299f6a89c23ed506e8118fac151e2bdc9018c"
defaults:

14
.circleci/osx_install_dependencies.sh
View File

@ -43,13 +43,13 @@ then
./scripts/install_obsolete_jsoncpp_1_7_4.sh
# z3
wget https://github.com/Z3Prover/z3/releases/download/z3-4.8.8/z3-4.8.8-x64-osx-10.14.6.zip
unzip z3-4.8.8-x64-osx-10.14.6.zip
rm -f z3-4.8.8-x64-osx-10.14.6.zip
cp z3-4.8.8-x64-osx-10.14.6/bin/libz3.a /usr/local/lib
cp z3-4.8.8-x64-osx-10.14.6/bin/z3 /usr/local/bin
cp z3-4.8.8-x64-osx-10.14.6/include/* /usr/local/include
rm -rf z3-4.8.8-x64-osx-10.14.6
wget https://github.com/Z3Prover/z3/releases/download/z3-4.8.9/z3-4.8.9-x64-osx-10.14.6.zip
unzip z3-4.8.9-x64-osx-10.14.6.zip
rm -f z3-4.8.9-x64-osx-10.14.6.zip
cp z3-4.8.9-x64-osx-10.14.6/bin/libz3.a /usr/local/lib
cp z3-4.8.9-x64-osx-10.14.6/bin/z3 /usr/local/bin
cp z3-4.8.9-x64-osx-10.14.6/include/* /usr/local/include
rm -rf z3-4.8.9-x64-osx-10.14.6
# evmone
wget https://github.com/ethereum/evmone/releases/download/v0.4.0/evmone-0.4.0-darwin-x86_64.tar.gz

2
.travis.yml
View File

@ -113,7 +113,7 @@ matrix:
before_install:
- nvm install 10
- nvm use 10
- docker pull solbuildpackpusher/solidity-buildpack-deps@sha256:d557d015918c3cf68b0d22839bab41013f0757b651a7fef21595f89721dbebcc
- docker pull solbuildpackpusher/solidity-buildpack-deps@sha256:23dad3b34deae8107c8551804ef299f6a89c23ed506e8118fac151e2bdc9018c
env:
- SOLC_EMSCRIPTEN=On
- SOLC_INSTALL_DEPS_TRAVIS=Off

2
scripts/build_emscripten.sh
View File

@ -35,5 +35,5 @@ else
fi
docker run -v $(pwd):/root/project -w /root/project \
solbuildpackpusher/solidity-buildpack-deps@sha256:d557d015918c3cf68b0d22839bab41013f0757b651a7fef21595f89721dbebcc \
solbuildpackpusher/solidity-buildpack-deps@sha256:23dad3b34deae8107c8551804ef299f6a89c23ed506e8118fac151e2bdc9018c\
./scripts/travis-emscripten/build_emscripten.sh $BUILD_DIR

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

@ -17,4 +17,5 @@ contract C
}
}
// ----
// Warning 1218: (297-321): Error trying to invoke SMT solver.
// Warning 4661: (297-321): Assertion violation happens here.

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

@ -20,4 +20,3 @@ contract LoopFor2 {
}
// ----
// Warning 6328: (363-382): Assertion violation happens here.
// Warning 4661: (316-336): Assertion violation happens here.

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

@ -21,4 +21,3 @@ contract LoopFor2 {
// ----
// Warning 6328: (341-360): Assertion violation happens here.
// Warning 6328: (364-383): Assertion violation happens here.
// Warning 4661: (317-337): Assertion violation happens here.

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

@ -15,4 +15,4 @@ contract C {
}
}
// ----
// Warning 4661: (143-169): Assertion violation happens here.
// Warning 6328: (143-169): Assertion violation happens here.