diff options
| author | Leonardo Alt <leonardoaltt@gmail.com> | 2018-01-21 20:58:56 +0800 |
|---|---|---|
| committer | Leonardo Alt <leonardoaltt@gmail.com> | 2018-03-13 03:16:47 +0800 |
| commit | 6a940f0a99e941c48e5deb695e89ac52784c4f3c (patch) | |
| tree | 547d592bca858c48dbdce61aafb2b71ac7369338 /test/libsolidity/SMTChecker.cpp | |
| parent | 886dc0512cba2c6bd6198eca88f1e84c55d392e5 (diff) | |
| download | dexon-solidity-6a940f0a99e941c48e5deb695e89ac52784c4f3c.tar dexon-solidity-6a940f0a99e941c48e5deb695e89ac52784c4f3c.tar.gz dexon-solidity-6a940f0a99e941c48e5deb695e89ac52784c4f3c.tar.bz2 dexon-solidity-6a940f0a99e941c48e5deb695e89ac52784c4f3c.tar.lz dexon-solidity-6a940f0a99e941c48e5deb695e89ac52784c4f3c.tar.xz dexon-solidity-6a940f0a99e941c48e5deb695e89ac52784c4f3c.tar.zst dexon-solidity-6a940f0a99e941c48e5deb695e89ac52784c4f3c.zip | |
[SMTChecker] Support to Bool variables
Diffstat (limited to 'test/libsolidity/SMTChecker.cpp')
| -rw-r--r-- | test/libsolidity/SMTChecker.cpp | 98 |
1 files changed, 98 insertions, 0 deletions
diff --git a/test/libsolidity/SMTChecker.cpp b/test/libsolidity/SMTChecker.cpp index 12b5f439..b97fc80e 100644 --- a/test/libsolidity/SMTChecker.cpp +++ b/test/libsolidity/SMTChecker.cpp @@ -329,6 +329,104 @@ 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); +} + +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 |