From a98edb22e57ba497ba1ec675e47439089ce9e140 Mon Sep 17 00:00:00 2001 From: Yoichi Hirai Date: Wed, 7 Sep 2016 18:30:53 +0200 Subject: 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 | 9 +++++++++ 1 file changed, 9 insertions(+) (limited to 'libsolidity') 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}); } -- cgit