diff options
| author | chriseth <c@ethdev.com> | 2016-05-10 20:30:24 +0800 |
|---|---|---|
| committer | chriseth <c@ethdev.com> | 2016-05-11 01:40:37 +0800 |
| commit | 656405240e08e47fce40a2f62af93abc758bd2d2 (patch) | |
| tree | ad1139d8209d5f98b41dee7eb82ebbd2d7d78495 /libsolidity/formal | |
| parent | cf226f0607386d1e6d9c75ebc7ce24e733ca4315 (diff) | |
| download | dexon-solidity-656405240e08e47fce40a2f62af93abc758bd2d2.tar dexon-solidity-656405240e08e47fce40a2f62af93abc758bd2d2.tar.gz dexon-solidity-656405240e08e47fce40a2f62af93abc758bd2d2.tar.bz2 dexon-solidity-656405240e08e47fce40a2f62af93abc758bd2d2.tar.lz dexon-solidity-656405240e08e47fce40a2f62af93abc758bd2d2.tar.xz dexon-solidity-656405240e08e47fce40a2f62af93abc758bd2d2.tar.zst dexon-solidity-656405240e08e47fce40a2f62af93abc758bd2d2.zip | |
Simplify interface of RationalNumber.
Diffstat (limited to 'libsolidity/formal')
| -rw-r--r-- | libsolidity/formal/Why3Translator.cpp | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/libsolidity/formal/Why3Translator.cpp b/libsolidity/formal/Why3Translator.cpp index 5921b9a4..c794cb24 100644 --- a/libsolidity/formal/Why3Translator.cpp +++ b/libsolidity/formal/Why3Translator.cpp @@ -431,7 +431,7 @@ bool Why3Translator::visit(BinaryOperation const& _binaryOperation) if (commonType.category() == Type::Category::RationalNumber) { auto const& constantNumber = dynamic_cast<RationalNumberType const&>(commonType); - if (constantNumber.denominator() != bigint(1)) + if (constantNumber.isFractional()) error(_binaryOperation, "Fractional numbers not supported."); add("(of_int " + toString(commonType.literalValue(nullptr)) + ")"); return false; @@ -595,7 +595,7 @@ bool Why3Translator::visit(Literal const& _literal) case Type::Category::RationalNumber: { auto const& constantNumber = dynamic_cast<RationalNumberType const&>(*type); - if (constantNumber.denominator() != 1) + if (constantNumber.isFractional()) error(_literal, "Fractional numbers not supported."); add("(of_int " + toString(type->literalValue(&_literal)) + ")"); break; |