cerc-io/solidity
11
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

changed names for Rational Constants and categories

Browse Source
This commit is contained in:
VoR0220
2016-05-09 11:41:02 -05:00
parent 4d283b2b30
commit 4b749fc333
6 changed files with 53 additions and 49 deletions
Download Patch File Download Diff File Expand all files Collapse all files
libsolidity/formal/Why3Translator.cpp
+4 -4
View File
@@ -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)) + ")");