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

[SMTChecker] Fix ICE when using >>>

Browse Source
This commit is contained in:
Djordje Mijovic 2020-10-28 09:25:14 +01:00
parent 07e3f60ffc
commit 9cc37c3fa4
2 changed files with 12 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
libsolidity/formal/SMTEncoder.cpp
View File

@ -1627,7 +1627,8 @@ smtutil::Expression SMTEncoder::bitwiseOperation(
result = bvLeft << bvRight; result = bvLeft << bvRight;
break; break;
case Token::SHR: case Token::SHR:
solAssert(false, ""); result = bvLeft >> bvRight;
break;
case Token::SAR: case Token::SAR:
result = isSigned ? result = isSigned ?
smtutil::Expression::ashr(bvLeft, bvRight) : smtutil::Expression::ashr(bvLeft, bvRight) :

10
test/libsolidity/smtCheckerTests/operators/shifts/shr_unused.sol Normal file
View File

@ -0,0 +1,10 @@
pragma experimental SMTChecker;
contract C {
function f() public pure {
fixed x;
assert(x >>> 6 == 0);
}
}
// ----
// UnimplementedFeatureError: Not yet implemented - FixedPointType.