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

Merge pull request #8746 from ethereum/smt_fix_fixed_point

Browse Source 
Fix ICE with fixed point
This commit is contained in:
Leonardo 2020-04-22 23:18:41 +02:00 committed by GitHub
commit 6d98b907ef
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
3 changed files with 8 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
Changelog.md
View File

@ -7,6 +7,7 @@ Compiler Features:
Bugfixes: Bugfixes:
* SMTChecker: Fix internal error when fixed points are used.
* Type Checker: Disallow ``virtual`` and ``override`` for constructors. * Type Checker: Disallow ``virtual`` and ``override`` for constructors.
* Type Checker: Fix several internal errors by performing size and recursiveness checks of types before the full type checking. * Type Checker: Fix several internal errors by performing size and recursiveness checks of types before the full type checking.
* Type Checker: Perform recursiveness check on structs declared at the file level. * Type Checker: Perform recursiveness check on structs declared at the file level.

5
libsolidity/formal/BMC.cpp
View File

@ -304,7 +304,10 @@ void BMC::endVisit(UnaryOperation const& _op)
{ {
SMTEncoder::endVisit(_op); SMTEncoder::endVisit(_op);
if (_op.annotation().type->category() == Type::Category::RationalNumber) if (
_op.annotation().type->category() == Type::Category::RationalNumber ||
_op.annotation().type->category() == Type::Category::FixedPoint
)
return; return;
switch (_op.getOperator()) switch (_op.getOperator())

3
libsolidity/formal/SMTEncoder.cpp
View File

@ -457,6 +457,9 @@ void SMTEncoder::endVisit(UnaryOperation const& _op)
createExpr(_op); createExpr(_op);
if (_op.annotation().type->category() == Type::Category::FixedPoint)
return;
switch (_op.getOperator()) switch (_op.getOperator())
{ {
case Token::Not: // ! case Token::Not: // !