diff options
| author | chriseth <chris@ethereum.org> | 2017-12-05 20:59:01 +0800 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2017-12-05 20:59:01 +0800 |
| commit | b47e023df166e2ab9fd085a29f74972b22c4897b (patch) | |
| tree | 63573be08cdc1fcf5005a314e67826c9baf7c7a1 /test | |
| parent | 240c79e61450d69f45356242924c23adf2a004b4 (diff) | |
| parent | 6d609557b6b2f13d7d8f8b13c2ceb1472266860a (diff) | |
| download | dexon-solidity-b47e023df166e2ab9fd085a29f74972b22c4897b.tar.gz dexon-solidity-b47e023df166e2ab9fd085a29f74972b22c4897b.tar.zst dexon-solidity-b47e023df166e2ab9fd085a29f74972b22c4897b.zip | |
Merge pull request #3032 from ethereum/division
Division and unary operators for SMT checker
Diffstat (limited to 'test')
| -rw-r--r-- | test/libsolidity/SMTChecker.cpp | 98 |
1 files changed, 96 insertions, 2 deletions
diff --git a/test/libsolidity/SMTChecker.cpp b/test/libsolidity/SMTChecker.cpp index 667d666b..38d02601 100644 --- a/test/libsolidity/SMTChecker.cpp +++ b/test/libsolidity/SMTChecker.cpp @@ -351,9 +351,9 @@ BOOST_AUTO_TEST_CASE(while_loop_simple) // Check that side-effects of condition are taken into account text = R"( contract C { - function f(uint x) public pure { + function f(uint x, uint y) public pure { x = 7; - while ((x = 5) > 0) { + while ((x = y) > 0) { } assert(x == 7); } @@ -458,6 +458,100 @@ BOOST_AUTO_TEST_CASE(for_loop) CHECK_WARNING(text, "Assertion violation"); } +BOOST_AUTO_TEST_CASE(division) +{ + string text = R"( + contract C { + function f(uint x, uint y) public pure returns (uint) { + return x / y; + } + } + )"; + CHECK_WARNING(text, "Division by zero"); + text = R"( + contract C { + function f(uint x, uint y) public pure returns (uint) { + require(y != 0); + return x / y; + } + } + )"; + CHECK_SUCCESS_NO_WARNINGS(text); + text = R"( + contract C { + function f(int x, int y) public pure returns (int) { + require(y != 0); + return x / y; + } + } + )"; + CHECK_WARNING(text, "Overflow"); + text = R"( + contract C { + function f(int x, int y) public pure returns (int) { + require(y != 0); + require(y != -1); + return x / y; + } + } + )"; + CHECK_SUCCESS_NO_WARNINGS(text); +} + +BOOST_AUTO_TEST_CASE(division_truncates_correctly) +{ + string text = R"( + contract C { + function f(uint x, uint y) public pure { + x = 7; + y = 2; + assert(x / y == 3); + } + } + )"; + CHECK_SUCCESS_NO_WARNINGS(text); + text = R"( + contract C { + function f(int x, int y) public pure { + x = 7; + y = 2; + assert(x / y == 3); + } + } + )"; + CHECK_SUCCESS_NO_WARNINGS(text); + text = R"( + contract C { + function f(int x, int y) public pure { + x = -7; + y = 2; + assert(x / y == -3); + } + } + )"; + CHECK_SUCCESS_NO_WARNINGS(text); + text = R"( + contract C { + function f(int x, int y) public pure { + x = 7; + y = -2; + assert(x / y == -3); + } + } + )"; + CHECK_SUCCESS_NO_WARNINGS(text); + text = R"( + contract C { + function f(int x, int y) public pure { + x = -7; + y = -2; + assert(x / y == 3); + } + } + )"; + CHECK_SUCCESS_NO_WARNINGS(text); +} + BOOST_AUTO_TEST_SUITE_END() } |