aboutsummaryrefslogtreecommitdiffstats
path: root/test/libsolidity/SMTChecker.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'test/libsolidity/SMTChecker.cpp')
-rw-r--r--test/libsolidity/SMTChecker.cpp487
1 files changed, 484 insertions, 3 deletions
diff --git a/test/libsolidity/SMTChecker.cpp b/test/libsolidity/SMTChecker.cpp
index 8d712a80..8c955292 100644
--- a/test/libsolidity/SMTChecker.cpp
+++ b/test/libsolidity/SMTChecker.cpp
@@ -42,7 +42,7 @@ public:
}
protected:
- virtual std::pair<SourceUnit const*, std::shared_ptr<Error const>>
+ virtual std::pair<SourceUnit const*, ErrorList>
parseAnalyseAndReturnError(
std::string const& _source,
bool _reportWarnings = false,
@@ -94,6 +94,7 @@ BOOST_AUTO_TEST_CASE(warn_on_typecast)
BOOST_AUTO_TEST_CASE(warn_on_struct)
{
string text = R"(
+ pragma experimental ABIEncoderV2;
contract C {
struct A { uint a; uint b; }
function f() public pure returns (A) {
@@ -101,8 +102,488 @@ BOOST_AUTO_TEST_CASE(warn_on_struct)
}
}
)";
- /// Multiple warnings, should check for: Assertion checker does not yet implement this expression.
- CHECK_WARNING_ALLOW_MULTI(text, "");
+ CHECK_WARNING_ALLOW_MULTI(text, (vector<string>{
+ "Assertion checker does not yet implement this expression.",
+ "Assertion checker does not yet support the type of this variable."
+ }));
+}
+
+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_merge_variables)
+{
+ // Branch does not touch variable a
+ 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);
+ // Positive branch touches variable a, but assertion should still hold.
+ text = R"(
+ contract C {
+ function f(uint x) public pure {
+ uint a = 3;
+ if (x > 10) {
+ a = 3;
+ }
+ assert(a == 3);
+ }
+ }
+ )";
+ CHECK_SUCCESS_NO_WARNINGS(text);
+ // Negative branch touches variable a, but assertion should still hold.
+ text = R"(
+ contract C {
+ function f(uint x) public pure {
+ uint a = 3;
+ if (x > 10) {
+ } else {
+ a = 3;
+ }
+ assert(a == 3);
+ }
+ }
+ )";
+ CHECK_SUCCESS_NO_WARNINGS(text);
+ // Variable is not merged, 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);
+ // Variable is reset in both branches
+ text = R"(
+ contract C {
+ function f(uint x) public pure {
+ uint a = 2;
+ if (x > 10) {
+ a = 3;
+ } else {
+ a = 3;
+ }
+ assert(a == 3);
+ }
+ }
+ )";
+ CHECK_SUCCESS_NO_WARNINGS(text);
+ // Variable is reset in both branches
+ text = R"(
+ contract C {
+ function f(uint x) public pure {
+ uint a = 2;
+ if (x > 10) {
+ a = 3;
+ } else {
+ a = 4;
+ }
+ 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);
+ text = R"(
+ contract C {
+ function f(uint x) public pure {
+ if (x > 10) {
+ assert(x > 9);
+ }
+ else if (x > 2)
+ {
+ assert(x <= 10 && x > 2);
+ }
+ else
+ {
+ assert(0 <= x && x <= 2);
+ }
+ }
+ }
+ )";
+ CHECK_SUCCESS_NO_WARNINGS(text);
+}
+
+BOOST_AUTO_TEST_CASE(ways_to_merge_variables)
+{
+ string 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;
+ }
+ 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, uint y) public pure {
+ x = 7;
+ while ((x = y) > 0) {
+ }
+ assert(x == 7);
+ }
+ }
+ )";
+ CHECK_WARNING(text, "Assertion violation happens here");
+}
+
+BOOST_AUTO_TEST_CASE(constant_condition)
+{
+ string text = R"(
+ contract C {
+ function f(uint x) public pure {
+ if (x >= 0) { revert(); }
+ }
+ }
+ )";
+ CHECK_WARNING(text, "Condition is always true");
+ text = R"(
+ contract C {
+ function f(uint x) public pure {
+ if (x >= 10) { if (x < 10) { revert(); } }
+ }
+ }
+ )";
+ CHECK_WARNING(text, "Condition is always false");
+ // a plain literal constant is fine
+ text = R"(
+ contract C {
+ function f(uint) public pure {
+ if (true) { revert(); }
+ }
+ }
+ )";
+ CHECK_SUCCESS_NO_WARNINGS(text);
+}
+
+
+BOOST_AUTO_TEST_CASE(for_loop)
+{
+ string text = R"(
+ contract C {
+ function f(uint x) public pure {
+ require(x == 2);
+ for (;;) {}
+ assert(x == 2);
+ }
+ }
+ )";
+ CHECK_SUCCESS_NO_WARNINGS(text);
+ text = R"(
+ contract C {
+ function f(uint x) public pure {
+ for (; x == 2; ) {
+ assert(x == 2);
+ }
+ }
+ }
+ )";
+ CHECK_SUCCESS_NO_WARNINGS(text);
+ text = R"(
+ contract C {
+ function f(uint x) public pure {
+ for (uint y = 2; x < 10; ) {
+ assert(y == 2);
+ }
+ }
+ }
+ )";
+ CHECK_SUCCESS_NO_WARNINGS(text);
+ text = R"(
+ contract C {
+ function f(uint x) public pure {
+ for (uint y = 2; x < 10; y = 3) {
+ assert(y == 2);
+ }
+ }
+ }
+ )";
+ CHECK_WARNING(text, "Assertion violation");
+ text = R"(
+ contract C {
+ function f(uint x) public pure {
+ for (uint y = 2; x < 10; ) {
+ y = 3;
+ }
+ assert(y == 3);
+ }
+ }
+ )";
+ CHECK_WARNING(text, "Assertion violation");
+ text = R"(
+ contract C {
+ function f(uint x) public pure {
+ for (uint y = 2; x < 10; ) {
+ y = 3;
+ }
+ assert(y == 2);
+ }
+ }
+ )";
+ 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()
generated by cgit v1.2.3 (git 2.25.1) at 2025-05-09 14:04:31 +0800