Translate mapping types into Why3 arrays when keys are integers

Even when the keys are signed the translation is supposed to work
because Why3 arrays allow negative indices.

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 "";
 }