cerc-io/solidity
10
0
Fork 0
mirror of https://github.com/ethereum/solidity synced 2023-10-03 13:03:40 +00:00
Code Issues Actions Packages Projects Releases Wiki Activity

Tests.

Browse Source
This commit is contained in:
chriseth 2017-09-29 10:30:12 +02:00 committed by Alex Beregszaszi
parent b37377641d
commit e5de4a66ed
2 changed files with 240 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
libsolidity/formal/SMTChecker.cpp
View File

@ -106,11 +106,6 @@ bool SMTChecker::visit(WhileStatement const& _node)
{
// TODO Check if condition is always true
// TODO Weird side effects like
// uint x = 1;
// while (x ++ > 0) { assert(x == 2); }
// solution: clear variables first, then execute and assert condition, then executed body.
auto touchedVariables = m_variableUsage->touchedVariables(_node);
resetVariables(touchedVariables);
if (_node.isDoWhile())

240
test/libsolidity/SMTChecker.cpp
View File

@ -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()
}