diff options
| author | VoR0220 <catalanor0220@gmail.com> | 2016-03-30 04:08:51 +0800 |
|---|---|---|
| committer | VoR0220 <catalanor0220@gmail.com> | 2016-05-10 00:41:02 +0800 |
| commit | 4b749fc33335cee2de50e31776ddae1f73649a7b (patch) | |
| tree | a8f28bbb649a1f4e80845aaef5a9b34c2f6c4f05 /libsolidity/formal/Why3Translator.cpp | |
| parent | 4d283b2b304f9c9a85fb6f03346cc7c9d0054daa (diff) | |
| download | dexon-solidity-4b749fc33335cee2de50e31776ddae1f73649a7b.tar dexon-solidity-4b749fc33335cee2de50e31776ddae1f73649a7b.tar.gz dexon-solidity-4b749fc33335cee2de50e31776ddae1f73649a7b.tar.bz2 dexon-solidity-4b749fc33335cee2de50e31776ddae1f73649a7b.tar.lz dexon-solidity-4b749fc33335cee2de50e31776ddae1f73649a7b.tar.xz dexon-solidity-4b749fc33335cee2de50e31776ddae1f73649a7b.tar.zst dexon-solidity-4b749fc33335cee2de50e31776ddae1f73649a7b.zip | |
changed names for Rational Constants and categories
Diffstat (limited to 'libsolidity/formal/Why3Translator.cpp')
| -rw-r--r-- | libsolidity/formal/Why3Translator.cpp | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/libsolidity/formal/Why3Translator.cpp b/libsolidity/formal/Why3Translator.cpp index e6f759aa..5921b9a4 100644 --- a/libsolidity/formal/Why3Translator.cpp +++ b/libsolidity/formal/Why3Translator.cpp @@ -428,9 +428,9 @@ bool Why3Translator::visit(BinaryOperation const& _binaryOperation) Type const& commonType = *_binaryOperation.annotation().commonType; Token::Value const c_op = _binaryOperation.getOperator(); - if (commonType.category() == Type::Category::NumberConstant) + if (commonType.category() == Type::Category::RationalNumber) { - auto const& constantNumber = dynamic_cast<ConstantNumberType const&>(commonType); + auto const& constantNumber = dynamic_cast<RationalNumberType const&>(commonType); if (constantNumber.denominator() != bigint(1)) error(_binaryOperation, "Fractional numbers not supported."); add("(of_int " + toString(commonType.literalValue(nullptr)) + ")"); @@ -592,9 +592,9 @@ bool Why3Translator::visit(Literal const& _literal) else add("true"); break; - case Type::Category::NumberConstant: + case Type::Category::RationalNumber: { - auto const& constantNumber = dynamic_cast<ConstantNumberType const&>(*type); + auto const& constantNumber = dynamic_cast<RationalNumberType const&>(*type); if (constantNumber.denominator() != 1) error(_literal, "Fractional numbers not supported."); add("(of_int " + toString(type->literalValue(&_literal)) + ")"); |