diff options
Diffstat (limited to 'test/libsolidity/smtCheckerTests/loops')
17 files changed, 177 insertions, 8 deletions
diff --git a/test/libsolidity/smtCheckerTests/loops/do_while_1_fail.sol b/test/libsolidity/smtCheckerTests/loops/do_while_1_fail.sol new file mode 100644 index 00000000..ea5bf044 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/loops/do_while_1_fail.sol @@ -0,0 +1,17 @@ +pragma experimental SMTChecker; + +contract C +{ + function f(uint x) public pure { + require(x < 100); + do { + // Overflows due to resetting x. + x = x + 1; + } while (x < 10); + assert(x < 14); + } +} +// ---- +// Warning: (150-155): Overflow (resulting value larger than 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff) happens here +// Warning: (146-155): Overflow (resulting value larger than 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff) happens here +// Warning: (179-193): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/loops/do_while_1_false_positives.sol b/test/libsolidity/smtCheckerTests/loops/do_while_1_false_positives.sol new file mode 100644 index 00000000..33e598b6 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/loops/do_while_1_false_positives.sol @@ -0,0 +1,19 @@ +pragma experimental SMTChecker; + +contract C +{ + function f(uint x) public pure { + require(x < 100); + do { + // Overflows due to resetting x. + x = x + 1; + } while (x < 1000); + // The assertion is true but we can't infer so + // because x is touched in the loop. + assert(x > 0); + } +} +// ---- +// Warning: (150-155): Overflow (resulting value larger than 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff) happens here +// Warning: (146-155): Overflow (resulting value larger than 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff) happens here +// Warning: (269-282): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/loops/for_1_fail.sol b/test/libsolidity/smtCheckerTests/loops/for_1_fail.sol new file mode 100644 index 00000000..3858403a --- /dev/null +++ b/test/libsolidity/smtCheckerTests/loops/for_1_fail.sol @@ -0,0 +1,17 @@ +pragma experimental SMTChecker; + +contract C +{ + function f(uint x) public pure { + require(x < 100); + for(uint i = 0; i < 10; ++i) { + // Overflows due to resetting x. + x = x + 1; + } + assert(x < 14); + } +} +// ---- +// Warning: (176-181): Overflow (resulting value larger than 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff) happens here +// Warning: (172-181): Overflow (resulting value larger than 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff) happens here +// Warning: (189-203): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/loops/for_1_false_positive.sol b/test/libsolidity/smtCheckerTests/loops/for_1_false_positive.sol new file mode 100644 index 00000000..7d7b7015 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/loops/for_1_false_positive.sol @@ -0,0 +1,18 @@ +pragma experimental SMTChecker; + +contract C +{ + function f(uint x) public pure { + require(x < 100); + for(uint i = 0; i < 10; ++i) { + // Overflows due to resetting x. + x = x + 1; + } + // The assertion is true but x is touched and reset. + assert(x > 0); + } +} +// ---- +// Warning: (176-181): Overflow (resulting value larger than 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff) happens here +// Warning: (172-181): Overflow (resulting value larger than 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff) happens here +// Warning: (244-257): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/loops/for_loop_5.sol b/test/libsolidity/smtCheckerTests/loops/for_loop_5.sol index 2c84960f..eb62d36e 100644 --- a/test/libsolidity/smtCheckerTests/loops/for_loop_5.sol +++ b/test/libsolidity/smtCheckerTests/loops/for_loop_5.sol @@ -9,4 +9,4 @@ contract C { } } // ---- -// Warning: (167-181): Assertion violation happens here\nNote that some information is erased after the execution of loops.\nYou can re-introduce information using require(). +// Warning: (167-181): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/loops/for_loop_6.sol b/test/libsolidity/smtCheckerTests/loops/for_loop_6.sol index 90c4c328..b0c3cae4 100644 --- a/test/libsolidity/smtCheckerTests/loops/for_loop_6.sol +++ b/test/libsolidity/smtCheckerTests/loops/for_loop_6.sol @@ -5,8 +5,9 @@ contract C { for (y = 2; x < 10; ) { y = 3; } - assert(y == 2); + // False positive due to resetting y. + assert(y < 4); } } // ---- -// Warning: (167-181): Assertion violation happens here\nNote that some information is erased after the execution of loops.\nYou can re-introduce information using require(). +// Warning: (213-226): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/loops/for_loop_trivial_condition_1.sol b/test/libsolidity/smtCheckerTests/loops/for_loop_trivial_condition_1.sol new file mode 100644 index 00000000..21e6c91e --- /dev/null +++ b/test/libsolidity/smtCheckerTests/loops/for_loop_trivial_condition_1.sol @@ -0,0 +1,10 @@ +pragma experimental SMTChecker; +contract C { + function f(uint x) public pure { + require(x == 2); + for (; x == 2;) {} + assert(x == 2); + } +} +// ---- +// Warning: (122-128): For loop condition is always true. diff --git a/test/libsolidity/smtCheckerTests/loops/for_loop_trivial_condition_2.sol b/test/libsolidity/smtCheckerTests/loops/for_loop_trivial_condition_2.sol new file mode 100644 index 00000000..6184c441 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/loops/for_loop_trivial_condition_2.sol @@ -0,0 +1,13 @@ +pragma experimental SMTChecker; +contract C { + function f(uint x) public pure { + require(x == 2); + uint y; + for (; x == 2;) { + y = 7; + } + assert(x == 2); + } +} +// ---- +// Warning: (138-144): For loop condition is always true. diff --git a/test/libsolidity/smtCheckerTests/loops/for_loop_trivial_condition_3.sol b/test/libsolidity/smtCheckerTests/loops/for_loop_trivial_condition_3.sol new file mode 100644 index 00000000..eec59ded --- /dev/null +++ b/test/libsolidity/smtCheckerTests/loops/for_loop_trivial_condition_3.sol @@ -0,0 +1,18 @@ +pragma experimental SMTChecker; +contract C { + function f(uint x) public pure { + require(x == 2); + uint y; + // The loop condition is always true, + // but since x is touched in the body + // we can't infer that. + for (; x == 2;) { + x = 2; + } + // False positive due to resetting x. + assert(x == 2); + } +} +// ---- +// Warning: (115-121): Unused local variable. +// Warning: (356-370): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/loops/for_loop_unreachable_1.sol b/test/libsolidity/smtCheckerTests/loops/for_loop_unreachable_1.sol new file mode 100644 index 00000000..f367d8d9 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/loops/for_loop_unreachable_1.sol @@ -0,0 +1,10 @@ +pragma experimental SMTChecker; +contract C { + function f(uint x) public pure { + require(x == 2); + for (; x > 2;) {} + assert(x == 2); + } +} +// ---- +// Warning: (122-127): For loop condition is always false. diff --git a/test/libsolidity/smtCheckerTests/loops/while_1.sol b/test/libsolidity/smtCheckerTests/loops/while_1.sol new file mode 100644 index 00000000..871ed929 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/loops/while_1.sol @@ -0,0 +1,17 @@ +pragma experimental SMTChecker; + +contract C +{ + function f(uint x, bool b) public pure { + require(x < 100); + while (x < 10) { + if (b) + x = x + 1; + else + x = 0; + } + assert(x > 0); + } +} +// ---- +// Warning: (177-190): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/loops/while_1_fail.sol b/test/libsolidity/smtCheckerTests/loops/while_1_fail.sol new file mode 100644 index 00000000..6964f7c8 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/loops/while_1_fail.sol @@ -0,0 +1,14 @@ +pragma experimental SMTChecker; + +contract C +{ + function f(uint x) public pure { + require(x < 100); + while (x < 10) { + x = x + 1; + } + assert(x < 14); + } +} +// ---- +// Warning: (139-153): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/loops/while_2_fail.sol b/test/libsolidity/smtCheckerTests/loops/while_2_fail.sol new file mode 100644 index 00000000..4c52287d --- /dev/null +++ b/test/libsolidity/smtCheckerTests/loops/while_2_fail.sol @@ -0,0 +1,15 @@ +pragma experimental SMTChecker; +contract C { + function f(uint x) public pure { + x = 2; + while (x > 1) { + if (x > 10) + x = 2; + else + x = 10; + } + assert(x == 2); + } +} +// ---- +// Warning: (158-172): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/loops/while_loop_simple_1.sol b/test/libsolidity/smtCheckerTests/loops/while_loop_simple_1.sol index 074be86f..9b5d04c3 100644 --- a/test/libsolidity/smtCheckerTests/loops/while_loop_simple_1.sol +++ b/test/libsolidity/smtCheckerTests/loops/while_loop_simple_1.sol @@ -4,10 +4,10 @@ contract C { function f(uint x) public pure { x = 2; while (x > 1) { - x = 2; + x = 1; } assert(x == 2); } } // ---- -// Warning: (194-208): Assertion violation happens here\nNote that some information is erased after the execution of loops.\nYou can re-introduce information using require(). +// Warning: (194-208): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/loops/while_loop_simple_3.sol b/test/libsolidity/smtCheckerTests/loops/while_loop_simple_3.sol index a37df888..f3634edb 100644 --- a/test/libsolidity/smtCheckerTests/loops/while_loop_simple_3.sol +++ b/test/libsolidity/smtCheckerTests/loops/while_loop_simple_3.sol @@ -8,4 +8,4 @@ contract C { } } // ---- -// Warning: (187-201): Assertion violation happens here\nNote that some information is erased after the execution of loops.\nYou can re-introduce information using require(). +// Warning: (187-201): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/loops/while_loop_simple_4.sol b/test/libsolidity/smtCheckerTests/loops/while_loop_simple_4.sol index f71da865..5a3aee9e 100644 --- a/test/libsolidity/smtCheckerTests/loops/while_loop_simple_4.sol +++ b/test/libsolidity/smtCheckerTests/loops/while_loop_simple_4.sol @@ -8,4 +8,4 @@ contract C { } } // ---- -// Warning: (199-213): Assertion violation happens here\nNote that some information is erased after the execution of loops.\nYou can re-introduce information using require(). +// Warning: (199-213): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/loops/while_loop_simple_5.sol b/test/libsolidity/smtCheckerTests/loops/while_loop_simple_5.sol index 41559c99..6c81e36f 100644 --- a/test/libsolidity/smtCheckerTests/loops/while_loop_simple_5.sol +++ b/test/libsolidity/smtCheckerTests/loops/while_loop_simple_5.sol @@ -9,4 +9,4 @@ contract C { } } // ---- -// Warning: (216-230): Assertion violation happens here\nNote that some information is erased after the execution of loops.\nYou can re-introduce information using require(). +// Warning: (216-230): Assertion violation happens here |