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 #8768 from ethereum/smt_revert_option

Browse Source 
Revert "Use Spacer option to improve performance of constant arrays"
This commit is contained in:
chriseth 2020-04-24 14:19:53 +02:00 committed by GitHub
commit 3bbd89e8e1
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
7 changed files with 9 additions and 23 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
libsolidity/formal/Z3CHCInterface.cpp
View File

@ -43,8 +43,6 @@ Z3CHCInterface::Z3CHCInterface():
p.set("fp.spacer.mbqi", false); p.set("fp.spacer.mbqi", false);
// Ground pobs by using values from a model. // Ground pobs by using values from a model.
p.set("fp.spacer.ground_pobs", false); p.set("fp.spacer.ground_pobs", false);
// Limits array reasoning, good for constant arrays.
p.set("fp.spacer.weak_abs", false);
m_solver.set(p); m_solver.set(p);
} }

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

@ -22,3 +22,4 @@ contract C
} }
} }
// ---- // ----
// Warning: (130-144): Error trying to invoke SMT solver.

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

@ -12,10 +12,12 @@ contract LoopFor2 {
b[i] = i + 1; b[i] = i + 1;
c[i] = b[i]; c[i] = b[i];
} }
// This is safe but too hard to solve currently.
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: (312-331): Assertion violation happens here // Warning: (316-336): Assertion violation happens here
// Warning: (363-382): Assertion violation happens here

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

@ -19,5 +19,6 @@ contract LoopFor2 {
} }
} }
// ---- // ----
// Warning: (317-337): Assertion violation happens here
// Warning: (341-360): Assertion violation happens here // Warning: (341-360): Assertion violation happens here
// Warning: (364-383): Assertion violation happens here // Warning: (364-383): 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

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

@ -16,5 +16,4 @@ contract C
// ==== // ====
// SMTSolvers: z3 // SMTSolvers: z3
// ---- // ----
// Warning: (174-194): Error trying to invoke SMT solver.
// Warning: (174-194): Assertion violation happens here // Warning: (174-194): Assertion violation happens here

17
test/libsolidity/smtCheckerTests/types/unused_mapping.sol
View File

@ -1,17 +0,0 @@
pragma experimental SMTChecker;
contract C {
uint x;
uint y;
mapping (address => bool) public never_used;
function inc() public {
require(x < 10);
require(y < 10);
if(x == 0) x = 0; // noop state var read
x++;
y++;
assert(y == x);
}
}