From 2dbb35d4a8fc4321d59a670343b439232c92eaa9 Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Wed, 18 Apr 2018 23:14:45 +0200 Subject: [SMTChecker] Support to integer and Bool storage vars --- test/libsolidity/SMTChecker.cpp | 66 +++++++++++++++++++++++++++++++++++++++++ 1 file changed, 66 insertions(+) (limited to 'test') diff --git a/test/libsolidity/SMTChecker.cpp b/test/libsolidity/SMTChecker.cpp index beb933a4..ce3569f3 100644 --- a/test/libsolidity/SMTChecker.cpp +++ b/test/libsolidity/SMTChecker.cpp @@ -467,6 +467,72 @@ BOOST_AUTO_TEST_CASE(bool_int_mixed) CHECK_SUCCESS_NO_WARNINGS(text); } +BOOST_AUTO_TEST_CASE(storage_value_vars) +{ + string text = R"( + contract C + { + address a; + bool b; + uint c; + function f(uint x) public { + if (x == 0) + { + a = 100; + b = true; + } + else + { + a = 200; + b = false; + } + assert(a > 0 && b); + } + } + )"; + CHECK_WARNING(text, "Assertion violation happens here"); + text = R"( + contract C + { + address a; + bool b; + uint c; + function f() public view { + assert(c > 0); + } + } + )"; + CHECK_WARNING(text, "Assertion violation happens here"); + text = R"( + contract C + { + address a; + bool b; + uint c; + function f(uint x) public { + if (x == 0) + { + a = 100; + b = true; + } + else + { + a = 200; + b = false; + } + assert(b == (a < 200)); + } + + function g() public view { + require(a < 100); + assert(c >= 0); + } + + } + )"; + CHECK_SUCCESS_NO_WARNINGS(text); +} + BOOST_AUTO_TEST_CASE(while_loop_simple) { // Check that variables are cleared -- cgit From 4117e859eb5780873177cf1c93eb8379e17ed247 Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Mon, 30 Apr 2018 16:30:41 +0200 Subject: [SMTChecker] Declaring all state vars before any function is visited --- test/libsolidity/SMTChecker.cpp | 11 +++++++++++ 1 file changed, 11 insertions(+) (limited to 'test') diff --git a/test/libsolidity/SMTChecker.cpp b/test/libsolidity/SMTChecker.cpp index ce3569f3..5f54db6d 100644 --- a/test/libsolidity/SMTChecker.cpp +++ b/test/libsolidity/SMTChecker.cpp @@ -531,6 +531,17 @@ BOOST_AUTO_TEST_CASE(storage_value_vars) } )"; CHECK_SUCCESS_NO_WARNINGS(text); + text = R"( + contract C + { + function f() public view { + assert(c > 0); + } + uint c; + } + )"; + CHECK_WARNING(text, "Assertion violation happens here"); + } BOOST_AUTO_TEST_CASE(while_loop_simple) -- cgit From a0b42105e49456faf89dd0d86cfba2a6219c514e Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Wed, 2 May 2018 15:52:23 +0200 Subject: Testing state vars that are declared after functions that use them --- test/libsolidity/SMTChecker.cpp | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) (limited to 'test') diff --git a/test/libsolidity/SMTChecker.cpp b/test/libsolidity/SMTChecker.cpp index 5f54db6d..71fdb906 100644 --- a/test/libsolidity/SMTChecker.cpp +++ b/test/libsolidity/SMTChecker.cpp @@ -506,9 +506,6 @@ BOOST_AUTO_TEST_CASE(storage_value_vars) text = R"( contract C { - address a; - bool b; - uint c; function f(uint x) public { if (x == 0) { @@ -527,7 +524,9 @@ BOOST_AUTO_TEST_CASE(storage_value_vars) require(a < 100); assert(c >= 0); } - + address a; + bool b; + uint c; } )"; CHECK_SUCCESS_NO_WARNINGS(text); -- cgit