diff options
Diffstat (limited to 'test/libsolidity/SMTChecker.cpp')
| -rw-r--r-- | test/libsolidity/SMTChecker.cpp | 240 |
1 files changed, 240 insertions, 0 deletions
diff --git a/test/libsolidity/SMTChecker.cpp b/test/libsolidity/SMTChecker.cpp index 8d712a80..400f696c 100644 --- a/test/libsolidity/SMTChecker.cpp +++ b/test/libsolidity/SMTChecker.cpp @@ -105,6 +105,246 @@ BOOST_AUTO_TEST_CASE(warn_on_struct) CHECK_WARNING_ALLOW_MULTI(text, ""); } +BOOST_AUTO_TEST_CASE(simple_assert) +{ + string text = R"( + contract C { + function f(uint a) public pure { assert(a == 2); } + } + )"; + CHECK_WARNING(text, "Assertion violation happens here for"); +} + +BOOST_AUTO_TEST_CASE(simple_assert_with_require) +{ + string text = R"( + contract C { + function f(uint a) public pure { require(a < 10); assert(a < 20); } + } + )"; + CHECK_SUCCESS_NO_WARNINGS(text); +} + +BOOST_AUTO_TEST_CASE(assignment_in_declaration) +{ + string text = R"( + contract C { + function f() public pure { uint a = 2; assert(a == 2); } + } + )"; + CHECK_SUCCESS_NO_WARNINGS(text); +} + +BOOST_AUTO_TEST_CASE(use_before_declaration) +{ + string text = R"( + contract C { + function f() public pure { a = 3; uint a = 2; assert(a == 2); } + } + )"; + CHECK_SUCCESS_NO_WARNINGS(text); + text = R"( + contract C { + function f() public pure { assert(a == 0); uint a = 2; assert(a == 2); } + } + )"; + CHECK_SUCCESS_NO_WARNINGS(text); +} + +BOOST_AUTO_TEST_CASE(function_call_does_not_clear_local_vars) +{ + string text = R"( + contract C { + function f() public { + uint a = 3; + this.f(); + assert(a == 3); + f(); + assert(a == 3); + } + } + )"; + CHECK_SUCCESS_NO_WARNINGS(text); +} + +BOOST_AUTO_TEST_CASE(branches_clear_variables) +{ + // Only clears accessed variables + string text = R"( + contract C { + function f(uint x) public pure { + uint a = 3; + if (x > 10) { + } + assert(a == 3); + } + } + )"; + CHECK_SUCCESS_NO_WARNINGS(text); + // It is just a plain clear and will not combine branches. + text = R"( + contract C { + function f(uint x) public pure { + uint a = 3; + if (x > 10) { + a = 3; + } + assert(a == 3); + } + } + )"; + CHECK_WARNING(text, "Assertion violation happens here"); + // Clear also works on the else branch + text = R"( + contract C { + function f(uint x) public pure { + uint a = 3; + if (x > 10) { + } else { + a = 3; + } + assert(a == 3); + } + } + )"; + CHECK_WARNING(text, "Assertion violation happens here"); + // Variable is not cleared, if it is only read. + text = R"( + contract C { + function f(uint x) public pure { + uint a = 3; + if (x > 10) { + assert(a == 3); + } else { + assert(a == 3); + } + assert(a == 3); + } + } + )"; + CHECK_SUCCESS_NO_WARNINGS(text); +} + +BOOST_AUTO_TEST_CASE(branches_assert_condition) +{ + string text = R"( + contract C { + function f(uint x) public pure { + if (x > 10) { + assert(x > 9); + } + else + { + assert(x < 11); + } + } + } + )"; + CHECK_SUCCESS_NO_WARNINGS(text); +} + +BOOST_AUTO_TEST_CASE(ways_to_clear_variables) +{ + string text = R"( + contract C { + function f(uint x) public pure { + uint a = 3; + if (x > 10) { + a++; + } + assert(a == 3); + } + } + )"; + text = R"( + contract C { + function f(uint x) public pure { + uint a = 3; + if (x > 10) { + ++a; + } + assert(a == 3); + } + } + )"; + CHECK_WARNING(text, "Assertion violation happens here"); + text = R"( + contract C { + function f(uint x) public pure { + uint a = 3; + if (x > 10) { + a = 5; + } + assert(a == 3); + } + } + )"; + CHECK_WARNING(text, "Assertion violation happens here"); +} + +BOOST_AUTO_TEST_CASE(while_loop_simple) +{ + // Check that variables are cleared + string text = R"( + contract C { + function f(uint x) public pure { + x = 2; + while (x > 1) { + x = 2; + } + assert(x == 2); + } + } + )"; + CHECK_WARNING(text, "Assertion violation happens here"); + // Check that condition is assumed. + text = R"( + contract C { + function f(uint x) public pure { + while (x == 2) { + assert(x == 2); + } + } + } + )"; + CHECK_SUCCESS_NO_WARNINGS(text); + // Check that condition is not assumed after the body anymore + text = R"( + contract C { + function f(uint x) public pure { + while (x == 2) { + } + assert(x == 2); + } + } + )"; + CHECK_WARNING(text, "Assertion violation happens here"); + // Check that negation of condition is not assumed after the body anymore + text = R"( + contract C { + function f(uint x) public pure { + while (x == 2) { + } + assert(x != 2); + } + } + )"; + CHECK_WARNING(text, "Assertion violation happens here"); + // Check that side-effects of condition are taken into account + text = R"( + contract C { + function f(uint x) public pure { + x = 7; + while ((x = 5) > 0) { + } + assert(x == 7); + } + } + )"; + CHECK_WARNING(text, "Assertion violation happens here"); +} + + BOOST_AUTO_TEST_SUITE_END() } |