mirror of
https://github.com/ethereum/solidity
synced 2023-10-03 13:03:40 +00:00
40 lines
1.2 KiB
Solidity
40 lines
1.2 KiB
Solidity
contract C {
|
|
function leftU(uint8 x, uint8 y) internal pure returns (uint8) {
|
|
return x << y;
|
|
}
|
|
|
|
function leftS(int8 x, uint8 y) internal pure returns (int8) {
|
|
return x << y;
|
|
}
|
|
|
|
function t() public pure {
|
|
assert(leftU(255, 8) == 0);
|
|
// Fails because the above is true.
|
|
assert(leftU(255, 8) == 1);
|
|
|
|
assert(leftU(255, 1) == 254);
|
|
// Fails because the above is true.
|
|
assert(leftU(255, 1) == 255);
|
|
|
|
assert(leftU(255, 0) == 255);
|
|
// Fails because the above is true.
|
|
assert(leftU(255, 0) == 0);
|
|
|
|
assert(leftS(1, 7) == -128);
|
|
// Fails because the above is true.
|
|
assert(leftS(1, 7) == 127);
|
|
|
|
assert(leftS(1, 6) == 64);
|
|
// Fails because the above is true.
|
|
assert(leftS(1, 6) == -64);
|
|
}
|
|
}
|
|
// ====
|
|
// SMTEngine: all
|
|
// ----
|
|
// Warning 6328: (307-333='assert(leftU(255, 8) == 1)'): CHC: Assertion violation happens here.
|
|
// Warning 6328: (408-436='assert(leftU(255, 1) == 255)'): CHC: Assertion violation happens here.
|
|
// Warning 6328: (511-537='assert(leftU(255, 0) == 0)'): CHC: Assertion violation happens here.
|
|
// Warning 6328: (611-637='assert(leftS(1, 7) == 127)'): CHC: Assertion violation happens here.
|
|
// Warning 6328: (709-735='assert(leftS(1, 6) == -64)'): CHC: Assertion violation happens here.
|