From c861cf579dc4c1303d6d215b5b31f930e1d6477e Mon Sep 17 00:00:00 2001 From: Yoichi Hirai Date: Wed, 7 Sep 2016 17:41:12 +0200 Subject: 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. --- libsolidity/formal/Why3Translator.cpp | 14 ++++++++++++++ 1 file changed, 14 insertions(+) (limited to 'libsolidity') 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(&_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(&_type)) + { + solAssert(mappingType->keyType(), "A mappingType misses a keyType."); + if (dynamic_cast(&*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 ""; } -- cgit v1.2.3