aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
-rw-r--r--libsolidity/formal/Why3Translator.cpp14
1 files changed, 14 insertions, 0 deletions
diff --git a/libsolidity/formal/Why3Translator.cpp b/libsolidity/formal/Why3Translator.cpp
index b441b150..9a4a5cf5 100644
--- a/libsolidity/formal/Why3Translator.cpp
+++ b/libsolidity/formal/Why3Translator.cpp
@@ -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 "";
}