[SMTChecker] Updating old and adding new tests for compound shift operators.

This commit is contained in:
Djordje Mijovic 2020-09-22 11:16:34 +02:00
parent 79f550dba9
commit 96bafb9ba3
4 changed files with 30 additions and 3 deletions

View File

@ -9,5 +9,3 @@ contract C {
}
}
// ----
// Warning 6328: (123-136): Assertion violation happens here.
// Warning 9149: (112-119): Assertion checker does not yet implement this assignment operator.

View File

@ -10,4 +10,3 @@ contract C {
}
// ----
// Warning 6328: (117-130): Assertion violation happens here.
// Warning 9149: (106-113): Assertion checker does not yet implement this assignment operator.

View File

@ -0,0 +1,15 @@
pragma experimental SMTChecker;
contract C {
function f(uint256 a, uint256 b) internal pure returns (uint256) {
a <<= b;
return a;
}
function t() public pure {
assert(f(0x4266, 0x0) == 0x4266);
assert(f(0x4266, 0x8) == 0x426600);
assert(f(0x4266, 0xf0) == 0x4266000000000000000000000000000000000000000000000000000000000000);
assert(f(0x4266, 0x4266) == 0);
}
}
// ----

View File

@ -0,0 +1,15 @@
pragma experimental SMTChecker;
contract C {
function f(uint256 a, uint256 b) internal pure returns (uint256) {
a >>= b;
return a;
}
function t() public pure {
assert(f(0x4266, 0) == 0x4266);
assert(f(0x4266, 0x8) == 0x42);
assert(f(0x4266, 0x11) == 0);
assert(f(57896044618658097711785492504343953926634992332820282019728792003956564819968, 5) == 1809251394333065553493296640760748560207343510400633813116524750123642650624);
}
}
// ----