cerc-io/solidity
16
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 more SMTChecker division tests

Browse Source
This commit is contained in:
Leonardo Alt 2019-12-04 13:17:05 +01:00
parent b870e4ea31
commit ae6cdc3442
6 changed files with 40 additions and 54 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

54
test/libsolidity/SMTChecker.cpp
View File

@ -59,60 +59,6 @@ protected:
BOOST_FIXTURE_TEST_SUITE(SMTChecker, SMTCheckerFramework)
BOOST_AUTO_TEST_CASE(division_truncates_correctly)
{
string text = R"(
contract C {
function f(uint x, uint y) public pure {
x = 7;
y = 2;
assert(x / y == 3);
}
}
)";
CHECK_SUCCESS_NO_WARNINGS(text);
text = R"(
contract C {
function f(int x, int y) public pure {
x = 7;
y = 2;
assert(x / y == 3);
}
}
)";
CHECK_SUCCESS_NO_WARNINGS(text);
text = R"(
contract C {
function f(int x, int y) public pure {
x = -7;
y = 2;
assert(x / y == -3);
}
}
)";
CHECK_SUCCESS_NO_WARNINGS(text);
text = R"(
contract C {
function f(int x, int y) public pure {
x = 7;
y = -2;
assert(x / y == -3);
}
}
)";
CHECK_SUCCESS_NO_WARNINGS(text);
text = R"(
contract C {
function f(int x, int y) public pure {
x = -7;
y = -2;
assert(x / y == 3);
}
}
)";
CHECK_SUCCESS_NO_WARNINGS(text);
}
BOOST_AUTO_TEST_CASE(compound_assignment_division)
{
string text = R"(

8
test/libsolidity/smtCheckerTests/operators/division_truncates_correctly_1.sol Normal file
View File

@ -0,0 +1,8 @@
pragma experimental SMTChecker;
contract C {
function f(uint x, uint y) public pure {
x = 7;
y = 2;
assert(x / y == 3);
}
}

8
test/libsolidity/smtCheckerTests/operators/division_truncates_correctly_2.sol Normal file
View File

@ -0,0 +1,8 @@
pragma experimental SMTChecker;
contract C {
function f(int x, int y) public pure {
x = 7;
y = 2;
assert(x / y == 3);
}
}

8
test/libsolidity/smtCheckerTests/operators/division_truncates_correctly_3.sol Normal file
View File

@ -0,0 +1,8 @@
pragma experimental SMTChecker;
contract C {
function f(int x, int y) public pure {
x = -7;
y = 2;
assert(x / y == -3);
}
}

8
test/libsolidity/smtCheckerTests/operators/division_truncates_correctly_4.sol Normal file
View File

@ -0,0 +1,8 @@
pragma experimental SMTChecker;
contract C {
function f(int x, int y) public pure {
x = 7;
y = -2;
assert(x / y == -3);
}
}

8
test/libsolidity/smtCheckerTests/operators/division_truncates_correctly_5.sol Normal file
View File

@ -0,0 +1,8 @@
pragma experimental SMTChecker;
contract C {
function f(int x, int y) public pure {
x = -7;
y = -2;
assert(x / y == 3);
}
}