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.

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