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 #7298 from ethereum/smt_fix_division

Browse Source 
[SMTChecker] Adapt division test for Z3 only
This commit is contained in:
Leonardo 2019-08-24 11:40:49 +02:00 committed by GitHub
commit bb104546e1
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
1 changed files with 3 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
test/libsolidity/SMTChecker.cpp
View File

@ -116,13 +116,15 @@ BOOST_AUTO_TEST_CASE(division)
if (a == 0) { if (a == 0) {
return 0; return 0;
} }
// TODO remove when SMTChecker sees that this code is the `else` of the `return`.
require(a != 0);
uint256 c = a * b; uint256 c = a * b;
require(c / a == b); require(c / a == b);
return c; return c;
} }
} }
)"; )";
CHECK_WARNING(text, "Division by zero"); CHECK_SUCCESS_OR_WARNING(text, "might happen");
text = R"( text = R"(
contract C { contract C {
function div(uint256 a, uint256 b) internal pure returns (uint256) { function div(uint256 a, uint256 b) internal pure returns (uint256) {