diff options
author | Leonardo Alt <leo@ethereum.org> | 2018-10-10 20:31:49 +0800 |
---|---|---|
committer | Leonardo Alt <leo@ethereum.org> | 2018-10-15 21:11:21 +0800 |
commit | e4851cf59eed8d39a4b95e1ce8181b52e5c66d78 (patch) | |
tree | a1f3be719b94b81608ff4bc7c20f0b93b6090c36 /test/libsolidity | |
parent | 88b1558862602049261b8530c6c7edcd23b96eb7 (diff) | |
download | dexon-solidity-e4851cf59eed8d39a4b95e1ce8181b52e5c66d78.tar dexon-solidity-e4851cf59eed8d39a4b95e1ce8181b52e5c66d78.tar.gz dexon-solidity-e4851cf59eed8d39a4b95e1ce8181b52e5c66d78.tar.bz2 dexon-solidity-e4851cf59eed8d39a4b95e1ce8181b52e5c66d78.tar.lz dexon-solidity-e4851cf59eed8d39a4b95e1ce8181b52e5c66d78.tar.xz dexon-solidity-e4851cf59eed8d39a4b95e1ce8181b52e5c66d78.tar.zst dexon-solidity-e4851cf59eed8d39a4b95e1ce8181b52e5c66d78.zip |
[SMTChecker] Inline calls to internal functions
Diffstat (limited to 'test/libsolidity')
20 files changed, 264 insertions, 7 deletions
diff --git a/test/libsolidity/SMTChecker.cpp b/test/libsolidity/SMTChecker.cpp index 1f6f765f..c7e60256 100644 --- a/test/libsolidity/SMTChecker.cpp +++ b/test/libsolidity/SMTChecker.cpp @@ -137,16 +137,17 @@ BOOST_AUTO_TEST_CASE(function_call_does_not_clear_local_vars) { string text = R"( contract C { - function f() public { + function g() public pure {} + function f() public view { uint a = 3; - this.f(); + this.g(); assert(a == 3); - f(); + g(); assert(a == 3); } } )"; - CHECK_SUCCESS_NO_WARNINGS(text); + CHECK_WARNING(text, "Assertion checker does not yet implement this type of function call"); } BOOST_AUTO_TEST_CASE(branches_merge_variables) @@ -569,7 +570,10 @@ BOOST_AUTO_TEST_CASE(constant_condition) } } )"; - CHECK_WARNING(text, "Condition is always true"); + CHECK_WARNING_ALLOW_MULTI(text, (vector<string>{ + "Condition is always true", + "Assertion checker does not yet implement this type of function call" + })); text = R"( contract C { function f(uint x) public pure { @@ -577,7 +581,10 @@ BOOST_AUTO_TEST_CASE(constant_condition) } } )"; - CHECK_WARNING(text, "Condition is always false"); + CHECK_WARNING_ALLOW_MULTI(text, (vector<string>{ + "Condition is always false", + "Assertion checker does not yet implement this type of function call" + })); // a plain literal constant is fine text = R"( contract C { @@ -586,7 +593,7 @@ BOOST_AUTO_TEST_CASE(constant_condition) } } )"; - CHECK_SUCCESS_NO_WARNINGS(text); + CHECK_WARNING(text, "Assertion checker does not yet implement this type of function call"); } diff --git a/test/libsolidity/smtCheckerTests/functions/functions_identity_1.sol b/test/libsolidity/smtCheckerTests/functions/functions_identity_1.sol new file mode 100644 index 00000000..25a42db6 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/functions/functions_identity_1.sol @@ -0,0 +1,13 @@ +pragma experimental SMTChecker; +contract C +{ + function h(uint x) public pure returns (uint) { + return x; + } + function g() public pure { + uint x; + x = h(42); + assert(x > 0); + } +} + diff --git a/test/libsolidity/smtCheckerTests/functions/functions_identity_1_fail.sol b/test/libsolidity/smtCheckerTests/functions/functions_identity_1_fail.sol new file mode 100644 index 00000000..a70aaf61 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/functions/functions_identity_1_fail.sol @@ -0,0 +1,15 @@ +pragma experimental SMTChecker; +contract C +{ + function h(uint x) public pure returns (uint) { + return x; + } + function g() public pure { + uint x; + x = h(0); + assert(x > 0); + } +} + +// ---- +// Warning: (161-174): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/functions/functions_identity_2.sol b/test/libsolidity/smtCheckerTests/functions/functions_identity_2.sol new file mode 100644 index 00000000..aff24b03 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/functions/functions_identity_2.sol @@ -0,0 +1,17 @@ +pragma experimental SMTChecker; +contract C +{ + function h(uint x) public pure returns (uint) { + return k(x); + } + + function k(uint x) public pure returns (uint) { + return x; + } + function g() public pure { + uint x; + x = h(2); + assert(x > 0); + } +} + diff --git a/test/libsolidity/smtCheckerTests/functions/functions_identity_2_fail.sol b/test/libsolidity/smtCheckerTests/functions/functions_identity_2_fail.sol new file mode 100644 index 00000000..9baeb935 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/functions/functions_identity_2_fail.sol @@ -0,0 +1,19 @@ +pragma experimental SMTChecker; +contract C +{ + function h(uint x) public pure returns (uint) { + return k(x); + } + + function k(uint x) public pure returns (uint) { + return x; + } + function g() public pure { + uint x; + x = h(0); + assert(x > 0); + } +} + +// ---- +// Warning: (229-242): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/functions/functions_identity_as_tuple.sol b/test/libsolidity/smtCheckerTests/functions/functions_identity_as_tuple.sol new file mode 100644 index 00000000..3793f411 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/functions/functions_identity_as_tuple.sol @@ -0,0 +1,14 @@ +pragma experimental SMTChecker; +contract C +{ + function h(uint x) public pure returns (uint) { + return x; + } + function g() public pure { + uint x; + x = (h)(42); + assert(x > 0); + } +} + +// ---- diff --git a/test/libsolidity/smtCheckerTests/functions/functions_identity_as_tuple_fail.sol b/test/libsolidity/smtCheckerTests/functions/functions_identity_as_tuple_fail.sol new file mode 100644 index 00000000..e3c80594 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/functions/functions_identity_as_tuple_fail.sol @@ -0,0 +1,15 @@ +pragma experimental SMTChecker; +contract C +{ + function h(uint x) public pure returns (uint) { + return x; + } + function g() public pure { + uint x; + x = (h)(0); + assert(x > 0); + } +} + +// ---- +// Warning: (163-176): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/functions/functions_recursive.sol b/test/libsolidity/smtCheckerTests/functions/functions_recursive.sol new file mode 100644 index 00000000..d2f8ab1d --- /dev/null +++ b/test/libsolidity/smtCheckerTests/functions/functions_recursive.sol @@ -0,0 +1,17 @@ +pragma experimental SMTChecker; +contract C +{ + uint a; + function g() public { + if (a > 0) + { + a = a - 1; + g(); + } + else + assert(a == 0); + } +} + +// ---- +// Warning: (111-114): Assertion checker does not support recursive function calls. diff --git a/test/libsolidity/smtCheckerTests/functions/functions_recursive_indirect.sol b/test/libsolidity/smtCheckerTests/functions/functions_recursive_indirect.sol new file mode 100644 index 00000000..d5b83f00 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/functions/functions_recursive_indirect.sol @@ -0,0 +1,26 @@ +pragma experimental SMTChecker; +contract C +{ + uint a; + function f() public { + if (a > 0) + { + a = a - 1; + g(); + } + else + assert(a == 0); + } + function g() public { + if (a > 0) + { + a = a - 1; + f(); + } + else + assert(a == 0); + } +} +// ---- +// Warning: (206-209): Assertion checker does not support recursive function calls. +// Warning: (111-114): Assertion checker does not support recursive function calls. diff --git a/test/libsolidity/smtCheckerTests/functions/functions_storage_var_1.sol b/test/libsolidity/smtCheckerTests/functions/functions_storage_var_1.sol new file mode 100644 index 00000000..2f7563dd --- /dev/null +++ b/test/libsolidity/smtCheckerTests/functions/functions_storage_var_1.sol @@ -0,0 +1,14 @@ +pragma experimental SMTChecker; +contract C +{ + uint a; + function f(uint x) public { + uint y; + a = (y = x); + } + function g() public { + f(1); + assert(a > 0); + } +} + diff --git a/test/libsolidity/smtCheckerTests/functions/functions_storage_var_1_fail.sol b/test/libsolidity/smtCheckerTests/functions/functions_storage_var_1_fail.sol new file mode 100644 index 00000000..ad735768 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/functions/functions_storage_var_1_fail.sol @@ -0,0 +1,16 @@ +pragma experimental SMTChecker; +contract C +{ + uint a; + function f(uint x) public { + uint y; + a = (y = x); + } + function g() public { + f(0); + assert(a > 0); + } +} + +// ---- +// Warning: (144-157): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/functions/functions_storage_var_2.sol b/test/libsolidity/smtCheckerTests/functions/functions_storage_var_2.sol new file mode 100644 index 00000000..2f95d8af --- /dev/null +++ b/test/libsolidity/smtCheckerTests/functions/functions_storage_var_2.sol @@ -0,0 +1,15 @@ +pragma experimental SMTChecker; +contract C +{ + uint a; + function f(uint x) public { + uint y; + a = (y = x); + } + function g() public { + f(1); + f(42); + assert(a > 1); + } +} + diff --git a/test/libsolidity/smtCheckerTests/functions/functions_storage_var_2_fail.sol b/test/libsolidity/smtCheckerTests/functions/functions_storage_var_2_fail.sol new file mode 100644 index 00000000..5d972f96 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/functions/functions_storage_var_2_fail.sol @@ -0,0 +1,17 @@ +pragma experimental SMTChecker; +contract C +{ + uint a; + function f(uint x) public { + uint y; + a = (y = x); + } + function g() public { + f(1); + f(0); + assert(a > 0); + } +} + +// ---- +// Warning: (152-165): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/functions/functions_trivial_condition_for.sol b/test/libsolidity/smtCheckerTests/functions/functions_trivial_condition_for.sol new file mode 100644 index 00000000..7693ad81 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/functions/functions_trivial_condition_for.sol @@ -0,0 +1,8 @@ +pragma experimental SMTChecker; + +contract C +{ + function f(bool x) public pure { require(x); for (;x;) {} } +} +// ---- +// Warning: (98-99): For loop condition is always true. diff --git a/test/libsolidity/smtCheckerTests/functions/functions_trivial_condition_for_only_call.sol b/test/libsolidity/smtCheckerTests/functions/functions_trivial_condition_for_only_call.sol new file mode 100644 index 00000000..ed1ad73a --- /dev/null +++ b/test/libsolidity/smtCheckerTests/functions/functions_trivial_condition_for_only_call.sol @@ -0,0 +1,7 @@ +pragma experimental SMTChecker; + +contract C +{ + function f(bool x) public pure { for (;x;) {} } + function g() public pure { f(true); } +} diff --git a/test/libsolidity/smtCheckerTests/functions/functions_trivial_condition_if.sol b/test/libsolidity/smtCheckerTests/functions/functions_trivial_condition_if.sol new file mode 100644 index 00000000..364fe8d1 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/functions/functions_trivial_condition_if.sol @@ -0,0 +1,7 @@ +pragma experimental SMTChecker; +contract C +{ + function f(bool x) public pure { require(x); if (x) {} } +} +// ---- +// Warning: (95-96): Condition is always true. diff --git a/test/libsolidity/smtCheckerTests/functions/functions_trivial_condition_require.sol b/test/libsolidity/smtCheckerTests/functions/functions_trivial_condition_require.sol new file mode 100644 index 00000000..e76badf2 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/functions/functions_trivial_condition_require.sol @@ -0,0 +1,8 @@ +pragma experimental SMTChecker; + +contract C +{ + function f(bool x) public pure { x = true; require(x); } +} +// ---- +// Warning: (98-99): Condition is always true. diff --git a/test/libsolidity/smtCheckerTests/functions/functions_trivial_condition_require_only_call.sol b/test/libsolidity/smtCheckerTests/functions/functions_trivial_condition_require_only_call.sol new file mode 100644 index 00000000..5cae940b --- /dev/null +++ b/test/libsolidity/smtCheckerTests/functions/functions_trivial_condition_require_only_call.sol @@ -0,0 +1,7 @@ +pragma experimental SMTChecker; + +contract C +{ + function f(bool x) public pure { require(x); } + function g() public pure { f(true); } +} diff --git a/test/libsolidity/smtCheckerTests/functions/functions_trivial_condition_while.sol b/test/libsolidity/smtCheckerTests/functions/functions_trivial_condition_while.sol new file mode 100644 index 00000000..66396dd8 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/functions/functions_trivial_condition_while.sol @@ -0,0 +1,8 @@ +pragma experimental SMTChecker; + +contract C +{ + function f(bool x) public pure { require(x); while (x) {} } +} +// ---- +// Warning: (99-100): While loop condition is always true. diff --git a/test/libsolidity/smtCheckerTests/functions/functions_trivial_condition_while_only_call.sol b/test/libsolidity/smtCheckerTests/functions/functions_trivial_condition_while_only_call.sol new file mode 100644 index 00000000..5000eeb6 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/functions/functions_trivial_condition_while_only_call.sol @@ -0,0 +1,7 @@ +pragma experimental SMTChecker; + +contract C +{ + function f(bool x) public pure { while (x) {} } + function g() public pure { f(true); } +} |