From e4851cf59eed8d39a4b95e1ce8181b52e5c66d78 Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Wed, 10 Oct 2018 14:31:49 +0200 Subject: [SMTChecker] Inline calls to internal functions --- .../functions/functions_identity_1.sol | 13 +++++++++++ .../functions/functions_identity_1_fail.sol | 15 +++++++++++++ .../functions/functions_identity_2.sol | 17 ++++++++++++++ .../functions/functions_identity_2_fail.sol | 19 ++++++++++++++++ .../functions/functions_identity_as_tuple.sol | 14 ++++++++++++ .../functions/functions_identity_as_tuple_fail.sol | 15 +++++++++++++ .../functions/functions_recursive.sol | 17 ++++++++++++++ .../functions/functions_recursive_indirect.sol | 26 ++++++++++++++++++++++ .../functions/functions_storage_var_1.sol | 14 ++++++++++++ .../functions/functions_storage_var_1_fail.sol | 16 +++++++++++++ .../functions/functions_storage_var_2.sol | 15 +++++++++++++ .../functions/functions_storage_var_2_fail.sol | 17 ++++++++++++++ .../functions/functions_trivial_condition_for.sol | 8 +++++++ .../functions_trivial_condition_for_only_call.sol | 7 ++++++ .../functions/functions_trivial_condition_if.sol | 7 ++++++ .../functions_trivial_condition_require.sol | 8 +++++++ ...nctions_trivial_condition_require_only_call.sol | 7 ++++++ .../functions_trivial_condition_while.sol | 8 +++++++ ...functions_trivial_condition_while_only_call.sol | 7 ++++++ 19 files changed, 250 insertions(+) create mode 100644 test/libsolidity/smtCheckerTests/functions/functions_identity_1.sol create mode 100644 test/libsolidity/smtCheckerTests/functions/functions_identity_1_fail.sol create mode 100644 test/libsolidity/smtCheckerTests/functions/functions_identity_2.sol create mode 100644 test/libsolidity/smtCheckerTests/functions/functions_identity_2_fail.sol create mode 100644 test/libsolidity/smtCheckerTests/functions/functions_identity_as_tuple.sol create mode 100644 test/libsolidity/smtCheckerTests/functions/functions_identity_as_tuple_fail.sol create mode 100644 test/libsolidity/smtCheckerTests/functions/functions_recursive.sol create mode 100644 test/libsolidity/smtCheckerTests/functions/functions_recursive_indirect.sol create mode 100644 test/libsolidity/smtCheckerTests/functions/functions_storage_var_1.sol create mode 100644 test/libsolidity/smtCheckerTests/functions/functions_storage_var_1_fail.sol create mode 100644 test/libsolidity/smtCheckerTests/functions/functions_storage_var_2.sol create mode 100644 test/libsolidity/smtCheckerTests/functions/functions_storage_var_2_fail.sol create mode 100644 test/libsolidity/smtCheckerTests/functions/functions_trivial_condition_for.sol create mode 100644 test/libsolidity/smtCheckerTests/functions/functions_trivial_condition_for_only_call.sol create mode 100644 test/libsolidity/smtCheckerTests/functions/functions_trivial_condition_if.sol create mode 100644 test/libsolidity/smtCheckerTests/functions/functions_trivial_condition_require.sol create mode 100644 test/libsolidity/smtCheckerTests/functions/functions_trivial_condition_require_only_call.sol create mode 100644 test/libsolidity/smtCheckerTests/functions/functions_trivial_condition_while.sol create mode 100644 test/libsolidity/smtCheckerTests/functions/functions_trivial_condition_while_only_call.sol (limited to 'test/libsolidity/smtCheckerTests/functions') 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); } +} -- cgit