cerc-io/solidity
10
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 #7682 from ethereum/smt_z3486_tests

Browse Source 
[SMTChecker] Update test expectations for z3 4.8.6
This commit is contained in:
Daniel Kirchner 2019-11-12 10:30:10 +01:00 committed by GitHub
commit 52a9de83f3
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
5 changed files with 18 additions and 38 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
.circleci/config.yml
View File

@ -431,12 +431,12 @@ jobs:
- checkout - checkout
- restore_cache: - restore_cache:
keys: keys:
- dependencies-osx-{{ .Branch }}-{{ checksum ".circleci/config.yml" }} - dependencies-osx-{{ .Branch }}-{{ checksum ".circleci/config.yml" }}-{{ checksum ".circleci/osx_install_dependencies.sh" }}
- run: - run:
name: Install build dependencies name: Install build dependencies
command: ./.circleci/osx_install_dependencies.sh command: ./.circleci/osx_install_dependencies.sh
- save_cache: - save_cache:
key: dependencies-osx-{{ .Branch }}-{{ checksum ".circleci/config.yml" }} key: dependencies-osx-{{ .Branch }}-{{ checksum ".circleci/config.yml" }}-{{ checksum ".circleci/osx_install_dependencies.sh" }}
paths: paths:
- /usr/local/bin - /usr/local/bin
- /usr/local/sbin - /usr/local/sbin
@ -459,7 +459,7 @@ jobs:
- checkout - checkout
- restore_cache: - restore_cache:
keys: keys:
- dependencies-osx-{{ .Branch }}-{{ checksum ".circleci/config.yml" }} - dependencies-osx-{{ .Branch }}-{{ checksum ".circleci/config.yml" }}-{{ checksum ".circleci/osx_install_dependencies.sh" }}
- attach_workspace: - attach_workspace:
at: build at: build
- run: *run_soltest - run: *run_soltest
@ -475,7 +475,7 @@ jobs:
- checkout - checkout
- restore_cache: - restore_cache:
keys: keys:
- dependencies-osx-{{ .Branch }}-{{ checksum ".circleci/config.yml" }} - dependencies-osx-{{ .Branch }}-{{ checksum ".circleci/config.yml" }}-{{ checksum ".circleci/osx_install_dependencies.sh" }}
- attach_workspace: - attach_workspace:
at: build at: build
- run: *run_cmdline_tests - run: *run_cmdline_tests

14
.circleci/osx_install_dependencies.sh
View File

@ -43,13 +43,13 @@ then
./scripts/install_obsolete_jsoncpp_1_7_4.sh ./scripts/install_obsolete_jsoncpp_1_7_4.sh
# z3 # z3
wget https://github.com/Z3Prover/z3/releases/download/Z3-4.8.5/z3-4.8.5-x64-osx-10.14.2.zip 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.5-x64-osx-10.14.2.zip unzip z3-4.8.6-x64-osx-10.14.6.zip
rm -f z3-4.8.5-x64-osx-10.14.2.zip rm -f z3-4.8.6-x64-osx-10.14.6.zip
cp z3-4.8.5-x64-osx-10.14.2/bin/libz3.a /usr/local/lib cp z3-4.8.6-x64-osx-10.14.6/bin/libz3.a /usr/local/lib
cp z3-4.8.5-x64-osx-10.14.2/bin/z3 /usr/local/bin cp z3-4.8.6-x64-osx-10.14.6/bin/z3 /usr/local/bin
cp z3-4.8.5-x64-osx-10.14.2/include/* /usr/local/include cp z3-4.8.6-x64-osx-10.14.6/include/* /usr/local/include
rm -rf z3-4.8.5-x64-osx-10.14.2 rm -rf z3-4.8.6-x64-osx-10.14.6
# evmone # evmone
wget https://github.com/ethereum/evmone/releases/download/v0.1.0/evmone-0.1.0-darwin-x86_64.tar.gz wget https://github.com/ethereum/evmone/releases/download/v0.1.0/evmone-0.1.0-darwin-x86_64.tar.gz

5
test/libsolidity/smtCheckerTests/invariants/loop_array_for.sol
View File

@ -7,10 +7,11 @@ contract Simple {
for (i = 0; i < n; ++i) for (i = 0; i < n; ++i)
a[i] = i; a[i] = i;
require(n > 1); require(n > 1);
// Assertion is safe but current solver version cannot solve it. // Assertion is safe but current solver version times out.
// Keep test for next solver release. // Keep test for next solver release.
assert(a[n-1] > a[n-2]); assert(a[n-1] > a[n-2]);
} }
} }
// ---- // ----
// Warning: (267-290): Assertion violation happens here // Warning: (261-284): Error trying to invoke SMT solver.
// Warning: (261-284): Assertion violation happens here

23
test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_storage_memory.sol
View File

@ -1,23 +0,0 @@
pragma experimental SMTChecker;
contract LoopFor2 {
uint[] b;
uint[] c;
function testUnboundedForLoop(uint n) public {
b[0] = 900;
uint[] memory a = b;
require(n > 0 && n < 100);
uint i;
while (i < n) {
b[i] = i + 1;
c[i] = b[i];
++i;
}
assert(b[0] == c[0]);
assert(a[0] == 900);
assert(b[0] == 900);
}
}
// ----
// Warning: (312-331): Assertion violation happens here

6
test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_storage_storage.sol
View File

@ -14,11 +14,13 @@ contract LoopFor2 {
c[i] = b[i]; c[i] = b[i];
++i; ++i;
} }
// Fails as false positive.
assert(b[0] == c[0]); assert(b[0] == c[0]);
assert(a[0] == 900); assert(a[0] == 900);
assert(b[0] == 900); assert(b[0] == 900);
} }
} }
// ---- // ----
// Warning: (290-309): Assertion violation happens here // Warning: (296-316): Assertion violation happens here
// Warning: (313-332): Assertion violation happens here // Warning: (320-339): Assertion violation happens here
// Warning: (343-362): Assertion violation happens here