diff options
| author | chriseth <chris@ethereum.org> | 2018-03-13 16:35:31 +0800 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-03-13 16:35:31 +0800 |
| commit | f2614be95f71a274db3c172661726dd007e90cf7 (patch) | |
| tree | e324d1751243949f308d27c372670cf8e0e393f8 /test | |
| parent | 886dc0512cba2c6bd6198eca88f1e84c55d392e5 (diff) | |
| parent | 9b64dc501da5c743b948e4dca844a6cd67766be1 (diff) | |
| download | dexon-solidity-f2614be95f71a274db3c172661726dd007e90cf7.tar.gz dexon-solidity-f2614be95f71a274db3c172661726dd007e90cf7.tar.zst dexon-solidity-f2614be95f71a274db3c172661726dd007e90cf7.zip | |
Merge pull request #3647 from leonardoalt/smt_bool
[SMTChecker] Support to Bool variables
Diffstat (limited to 'test')
| -rw-r--r-- | test/libsolidity/SMTChecker.cpp | 138 |
1 files changed, 138 insertions, 0 deletions
diff --git a/test/libsolidity/SMTChecker.cpp b/test/libsolidity/SMTChecker.cpp index 12b5f439..beb933a4 100644 --- a/test/libsolidity/SMTChecker.cpp +++ b/test/libsolidity/SMTChecker.cpp @@ -329,6 +329,144 @@ BOOST_AUTO_TEST_CASE(ways_to_merge_variables) CHECK_WARNING(text, "Assertion violation happens here"); } +BOOST_AUTO_TEST_CASE(bool_simple) +{ + string text = R"( + contract C { + function f(bool x) public pure { + assert(x); + } + } + )"; + CHECK_WARNING(text, "Assertion violation happens here"); + text = R"( + contract C { + function f(bool x, bool y) public pure { + assert(x == y); + } + } + )"; + CHECK_WARNING(text, "Assertion violation happens here"); + text = R"( + contract C { + function f(bool x, bool y) public pure { + bool z = x || y; + assert(!(x && y) || z); + } + } + )"; + CHECK_SUCCESS_NO_WARNINGS(text); + text = R"( + contract C { + function f(bool x) public pure { + if(x) { + assert(x); + } else { + assert(!x); + } + } + } + )"; + CHECK_SUCCESS_NO_WARNINGS(text); + text = R"( + contract C { + function f(bool x) public pure { + bool y = x; + assert(x == y); + } + } + )"; + CHECK_SUCCESS_NO_WARNINGS(text); + text = R"( + contract C { + function f(bool x) public pure { + require(x); + bool y; + y = false; + assert(x || y); + } + } + )"; + CHECK_SUCCESS_NO_WARNINGS(text); + text = R"( + contract C { + function f(bool x) public pure { + bool y; + assert(x <= y); + } + } + )"; + CHECK_WARNING(text, "Assertion violation happens here"); + text = R"( + contract C { + function f(bool x) public pure { + bool y; + assert(x >= y); + } + } + )"; + CHECK_SUCCESS_NO_WARNINGS(text); + text = R"( + contract C { + function f(bool x) public pure { + require(x); + bool y; + assert(x > y); + assert(y < x); + } + } + )"; + CHECK_SUCCESS_NO_WARNINGS(text); +} + +BOOST_AUTO_TEST_CASE(bool_int_mixed) +{ + string text = R"( + contract C { + function f(bool x) public pure { + uint a; + if(x) + a = 1; + assert(!x || a > 0); + } + } + )"; + CHECK_SUCCESS_NO_WARNINGS(text); + text = R"( + contract C { + function f(bool x, uint a) public pure { + require(!x || a > 0); + uint b = a; + assert(!x || b > 0); + } + } + )"; + CHECK_SUCCESS_NO_WARNINGS(text); + text = R"( + contract C { + function f(bool x, bool y) public pure { + uint a; + if (x) { + if (y) { + a = 0; + } else { + a = 1; + } + } else { + if (y) { + a = 1; + } else { + a = 0; + } + } + bool xor_x_y = (x && !y) || (!x && y); + assert(!xor_x_y || a > 0); + } + } + )"; + CHECK_SUCCESS_NO_WARNINGS(text); +} + BOOST_AUTO_TEST_CASE(while_loop_simple) { // Check that variables are cleared |