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

Translate mapping types into Why3 arrays when keys are integers

Browse Source 
Even when the keys are signed the translation is supposed to work
because Why3 arrays allow negative indices.
This commit is contained in:
Yoichi Hirai 2016-09-07 17:41:12 +02:00
parent 00e8b059ea
commit c861cf579d
1 changed files with 14 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

14
libsolidity/formal/Why3Translator.cpp
View File

@ -77,12 +77,26 @@ string Why3Translator::toFormalType(Type const& _type) const
return "uint256";
}
else if (auto type = dynamic_cast<ArrayType const*>(&_type))
{
if (!type->isByteArray() && type->isDynamicallySized() && type->dataStoredIn(DataLocation::Memory))
{
string base = toFormalType(*type->baseType());
if (!base.empty())
return "array " + base;
}
}
else if (auto mappingType = dynamic_cast<MappingType const*>(&_type))
{
solAssert(mappingType->keyType(), "A mappingType misses a keyType.");
if (dynamic_cast<IntegerType const*>(&*mappingType->keyType()))
{
//@TODO Use the information from the key type and specify the length of the array as an invariant.
// Also the constructor need to specify the length of the array.
string valueType = toFormalType(*mappingType->valueType());
if (!valueType.empty())
return "array " + valueType;
}
}
return "";
}