diff options
Diffstat (limited to 'test/libsolidity/smtCheckerTests')
19 files changed, 250 insertions, 0 deletions
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); } +} |