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

Extract SMTChecker compound assignment division tests

Browse Source
This commit is contained in:
Leonardo Alt 2019-12-04 13:20:43 +01:00
parent ae6cdc3442
commit 02343208ad
4 changed files with 38 additions and 42 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

42
test/libsolidity/SMTChecker.cpp
View File

@ -59,48 +59,6 @@ protected:
BOOST_FIXTURE_TEST_SUITE(SMTChecker, SMTCheckerFramework) BOOST_FIXTURE_TEST_SUITE(SMTChecker, SMTCheckerFramework)
BOOST_AUTO_TEST_CASE(compound_assignment_division)
{
string text = R"(
contract C {
function f(uint x) public pure {
require(x == 2);
uint y = 10;
y /= y / x;
assert(y == x);
assert(y == 0);
}
}
)";
CHECK_WARNING(text, "Assertion violation");
text = R"(
contract C {
uint[] array;
function f(uint x, uint p) public {
require(x == 2);
array[p] = 10;
array[p] /= array[p] / x;
assert(array[p] == x);
assert(array[p] == 0);
}
}
)";
CHECK_WARNING(text, "Assertion violation");
text = R"(
contract C {
mapping (uint => uint) map;
function f(uint x, uint p) public {
require(x == 2);
map[p] = 10;
map[p] /= map[p] / x;
assert(map[p] == x);
assert(map[p] == 0);
}
}
)";
CHECK_WARNING(text, "Assertion violation");
}
BOOST_AUTO_TEST_CASE(mod) BOOST_AUTO_TEST_CASE(mod)
{ {
string text = R"( string text = R"(

12
test/libsolidity/smtCheckerTests/operators/compound_assignment_division_1.sol Normal file
View File

@ -0,0 +1,12 @@
pragma experimental SMTChecker;
contract C {
function f(uint x) public pure {
require(x == 2);
uint y = 10;
y /= y / x;
assert(y == x);
assert(y == 0);
}
}
// ----
// Warning: (147-161): Assertion violation happens here

13
test/libsolidity/smtCheckerTests/operators/compound_assignment_division_2.sol Normal file
View File

@ -0,0 +1,13 @@
pragma experimental SMTChecker;
contract C {
uint[] array;
function f(uint x, uint p) public {
require(x == 2);
array[p] = 10;
array[p] /= array[p] / x;
assert(array[p] == x);
assert(array[p] == 0);
}
}
// ----
// Warning: (188-209): Assertion violation happens here

13
test/libsolidity/smtCheckerTests/operators/compound_assignment_division_3.sol Normal file
View File

@ -0,0 +1,13 @@
pragma experimental SMTChecker;
contract C {
mapping (uint => uint) map;
function f(uint x, uint p) public {
require(x == 2);
map[p] = 10;
map[p] /= map[p] / x;
assert(map[p] == x);
assert(map[p] == 0);
}
}
// ----
// Warning: (194-213): Assertion violation happens here