diff --git a/.circleci/config.yml b/.circleci/config.yml index 87236581a..2139fa94d 100644 --- a/.circleci/config.yml +++ b/.circleci/config.yml @@ -9,7 +9,7 @@ version: 2.1 parameters: docker-image-rev: type: string - default: "2" + default: "3" defaults: diff --git a/.circleci/docker/Dockerfile.clang.ubuntu1904 b/.circleci/docker/Dockerfile.clang.ubuntu1904 index 3678afbed..0306dcf68 100644 --- a/.circleci/docker/Dockerfile.clang.ubuntu1904 +++ b/.circleci/docker/Dockerfile.clang.ubuntu1904 @@ -62,7 +62,7 @@ RUN git clone --recursive -b boost-1.69.0 https://github.com/boostorg/boost.git rm -rf /usr/src/boost # Z3 -RUN git clone --depth 1 -b z3-4.8.6 https://github.com/Z3Prover/z3.git \ +RUN git clone --depth 1 -b z3-4.8.7 https://github.com/Z3Prover/z3.git \ /usr/src/z3; \ cd /usr/src/z3; \ python scripts/mk_make.py --prefix=/usr ; \ diff --git a/.circleci/osx_install_dependencies.sh b/.circleci/osx_install_dependencies.sh index fadff605e..59e7c2234 100755 --- a/.circleci/osx_install_dependencies.sh +++ b/.circleci/osx_install_dependencies.sh @@ -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.6/z3-4.8.6-x64-osx-10.14.6.zip - unzip z3-4.8.6-x64-osx-10.14.6.zip - rm -f z3-4.8.6-x64-osx-10.14.6.zip - cp z3-4.8.6-x64-osx-10.14.6/bin/libz3.a /usr/local/lib - cp z3-4.8.6-x64-osx-10.14.6/bin/z3 /usr/local/bin - cp z3-4.8.6-x64-osx-10.14.6/include/* /usr/local/include - rm -rf z3-4.8.6-x64-osx-10.14.6 + wget https://github.com/Z3Prover/z3/releases/download/z3-4.8.7/z3-4.8.7-x64-osx-10.14.6.zip + unzip z3-4.8.7-x64-osx-10.14.6.zip + rm -f z3-4.8.7-x64-osx-10.14.6.zip + cp z3-4.8.7-x64-osx-10.14.6/bin/libz3.a /usr/local/lib + cp z3-4.8.7-x64-osx-10.14.6/bin/z3 /usr/local/bin + cp z3-4.8.7-x64-osx-10.14.6/include/* /usr/local/include + rm -rf z3-4.8.7-x64-osx-10.14.6 # evmone wget https://github.com/ethereum/evmone/releases/download/v0.3.0/evmone-0.3.0-darwin-x86_64.tar.gz diff --git a/test/libsolidity/smtCheckerTests/invariants/loop_array.sol b/test/libsolidity/smtCheckerTests/invariants/loop_array.sol deleted file mode 100644 index 0f6937d36..000000000 --- a/test/libsolidity/smtCheckerTests/invariants/loop_array.sol +++ /dev/null @@ -1,19 +0,0 @@ -pragma experimental SMTChecker; - -contract Simple { - uint[] a; - function f(uint n) public { - uint i; - while (i < n) - { - a[i] = i; - ++i; - } - require(n > 1); - // Assertion is safe but current solver version cannot solve it. - // Keep test for next solver release. - assert(a[n-1] > a[n-2]); - } -} -// ---- -// Warning: (273-296): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_storage_storage.sol b/test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_storage_storage.sol new file mode 100644 index 000000000..92d1ded3e --- /dev/null +++ b/test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_storage_storage.sol @@ -0,0 +1,26 @@ +pragma experimental SMTChecker; + +contract LoopFor2 { + uint[] b; + uint[] c; + + function testUnboundedForLoop(uint n) public { + b[0] = 900; + uint[] storage a = b; + require(n > 0 && n < 100); + uint i; + while (i < n) { + b[i] = i + 1; + c[i] = b[i]; + ++i; + } + // Fails as false positive. + assert(b[0] == c[0]); + assert(a[0] == 900); + assert(b[0] == 900); + } +} +// ---- +// Warning: (296-316): Assertion violation happens here +// Warning: (320-339): Assertion violation happens here +// Warning: (343-362): Assertion violation happens here