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 that used to give false negatives

Browse Source
This commit is contained in:
Leonardo Alt 2019-03-25 16:15:19 +01:00
parent 1d63b97857
commit 2764d2f525
3 changed files with 65 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

19
test/libsolidity/smtCheckerTests/functions/function_inside_branch_modify_state_var.sol Normal file
View File

@ -0,0 +1,19 @@
pragma experimental SMTChecker;
contract C
{
uint x;
function f() internal {
require(x < 10000);
x = x + 1;
}
function g(bool b) public {
x = 0;
if (b)
f();
// Should fail for `b == true`.
assert(x == 0);
}
}
// ----
// Warning: (209-223): Assertion violation happens here

18
test/libsolidity/smtCheckerTests/functions/function_inside_branch_modify_state_var_2.sol Normal file
View File

@ -0,0 +1,18 @@
pragma experimental SMTChecker;
contract C
{
uint x;
function f() internal {
require(x < 10000);
x = x + 1;
}
function g(bool b) public {
x = 0;
if (b)
f();
else
f();
assert(x == 1);
}
}

28
test/libsolidity/smtCheckerTests/functions/function_inside_branch_modify_state_var_3.sol Normal file
View File

@ -0,0 +1,28 @@
pragma experimental SMTChecker;
contract C
{
uint x;
function f() internal {
require(x < 10000);
x = x + 1;
}
function g(bool b) public {
x = 0;
if (b)
f();
// Should fail for `b == true`.
assert(x == 0);
}
function h(bool b) public {
x = 0;
if (!b)
f();
// Should fail for `b == false`.
assert(x == 0);
}
}
// ----
// Warning: (209-223): Assertion violation happens here
// Warning: (321-335): Assertion violation happens here