diff options
Diffstat (limited to 'libsolidity/formal/Why3Translator.cpp')
| -rw-r--r-- | libsolidity/formal/Why3Translator.cpp | 12 |
1 files changed, 10 insertions, 2 deletions
diff --git a/libsolidity/formal/Why3Translator.cpp b/libsolidity/formal/Why3Translator.cpp index 24fbab13..e6f759aa 100644 --- a/libsolidity/formal/Why3Translator.cpp +++ b/libsolidity/formal/Why3Translator.cpp @@ -428,8 +428,11 @@ bool Why3Translator::visit(BinaryOperation const& _binaryOperation) Type const& commonType = *_binaryOperation.annotation().commonType; Token::Value const c_op = _binaryOperation.getOperator(); - if (commonType.category() == Type::Category::IntegerConstant) + if (commonType.category() == Type::Category::NumberConstant) { + auto const& constantNumber = dynamic_cast<ConstantNumberType const&>(commonType); + if (constantNumber.denominator() != bigint(1)) + error(_binaryOperation, "Fractional numbers not supported."); add("(of_int " + toString(commonType.literalValue(nullptr)) + ")"); return false; } @@ -589,9 +592,14 @@ bool Why3Translator::visit(Literal const& _literal) else add("true"); break; - case Type::Category::IntegerConstant: + case Type::Category::NumberConstant: + { + auto const& constantNumber = dynamic_cast<ConstantNumberType const&>(*type); + if (constantNumber.denominator() != 1) + error(_literal, "Fractional numbers not supported."); add("(of_int " + toString(type->literalValue(&_literal)) + ")"); break; + } default: error(_literal, "Not supported."); } |