in Sources/SolToBoogie/TransUtils.cs [282:437]
public static BoogieType GetBoogieTypeFromSolidityTypeName(TypeName type)
{
if (type is ElementaryTypeName elementaryType)
{
string typeString = elementaryType.TypeDescriptions.TypeString;
switch (typeString)
{
case "uint256":
case "uint248":
case "uint240":
case "uint232":
case "uint224":
case "uint216":
case "uint208":
case "uint200":
case "uint192":
case "uint184":
case "uint176":
case "uint168":
case "uint160":
case "uint152":
case "uint144":
case "uint136":
case "uint128":
case "uint120":
case "uint112":
case "uint104":
case "uint96":
case "uint88":
case "uint80":
case "uint72":
case "uint64":
case "uint56":
case "uint48":
case "uint40":
case "uint32":
case "uint24":
case "uint16":
case "uint8":
case "int256":
case "int248":
case "int240":
case "int232":
case "int224":
case "int216":
case "int208":
case "int200":
case "int192":
case "int184":
case "int176":
case "int168":
case "int160":
case "int152":
case "int144":
case "int136":
case "int128":
case "int120":
case "int112":
case "int104":
case "int96":
case "int88":
case "int80":
case "int72":
case "int64":
case "int56":
case "int48":
case "int40":
case "int32":
case "int24":
case "int16":
case "int8":
case "uint":
case "int":
return BoogieType.Int;
case "bool":
return BoogieType.Bool;
case "string":
return BoogieType.Int;
case "address":
case "address payable":
return BoogieType.Ref;
case "bytes1":
case "bytes2":
case "bytes3":
case "bytes4":
case "bytes5":
case "bytes6":
case "bytes7":
case "bytes8":
case "bytes9":
case "bytes10":
case "bytes11":
case "bytes12":
case "bytes13":
case "bytes14":
case "bytes15":
case "bytes16":
case "bytes17":
case "bytes18":
case "bytes19":
case "bytes20":
case "bytes21":
case "bytes22":
case "bytes23":
case "bytes24":
case "bytes25":
case "bytes26":
case "bytes27":
case "bytes28":
case "bytes29":
case "bytes30":
case "bytes31":
case "bytes32":
case "bytes":
return BoogieType.Int;
default:
throw new SystemException($"Unknown elementary type name: {type}");
}
}
else if (type is UserDefinedTypeName udt)
{
string typeString = udt.TypeDescriptions.TypeString;
if (udt.TypeDescriptions.IsEnum())
{
// model enum type using integers
return BoogieType.Int;
}
else if (udt.TypeDescriptions.IsContract())
{
string contractName = typeString.Substring("contract ".Length);
// model contract type using Ref
return BoogieType.Ref;
}
else if (udt.TypeDescriptions.IsStruct())
{
string contractName = typeString.Substring("struct ".Length);
return BoogieType.Ref;
}
else
{
throw new SystemException($"Unknown type name: {typeString}");
}
}
else if (type is Mapping mapping)
{
return BoogieType.Ref;
}
else if (type is ArrayTypeName array)
{
return BoogieType.Ref;
}
else
{
throw new SystemException($"Unknown type name: {type}");
}
}