Add Address module in the WhyML prelude

In the `--formal` output, this commit adds a module called `Address`,
which defines the address type as unsigned integer type bounded at
2^160-1.

1 files changed, 9 insertions, 0 deletions

diff --git a/libsolidity/formal/Why3Translator.cpp b/libsolidity/formal/Why3Translator.cpp
index 834024fa..b441b150 100644
--- a/libsolidity/formal/Why3Translator.cpp
+++ b/libsolidity/formal/Why3Translator.cpp
@@ -798,5 +798,14 @@ module UInt256
 		type t = uint256,
 		constant max = max_uint256
 end
+
+module Address
+	use import mach.int.Unsigned
+	type address
+	constant max_address: int = 0xffffffffffffffffffffffffffffffffffffffff (* 160 bit = 40 f's *)
+	clone export mach.int.Unsigned with
+		type t = address,
+		constant max = max_address
+end
    )", 0});
 }