aboutsummaryrefslogtreecommitdiffstats
path: root/libsolidity
diff options
context:
space:
mode:
authorYoichi Hirai <i@yoichihirai.com>2016-09-08 00:30:53 +0800
committerYoichi Hirai <i@yoichihirai.com>2016-09-08 02:39:23 +0800
commita98edb22e57ba497ba1ec675e47439089ce9e140 (patch)
treea6a192f247ea2befb3beeee51ce7c5f7e9abf5f5 /libsolidity
parentce11580988b6aae22845fbebfb09eb9c3881b250 (diff)
downloaddexon-solidity-a98edb22e57ba497ba1ec675e47439089ce9e140.tar.gz
dexon-solidity-a98edb22e57ba497ba1ec675e47439089ce9e140.tar.zst
dexon-solidity-a98edb22e57ba497ba1ec675e47439089ce9e140.zip
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.
Diffstat (limited to 'libsolidity')
-rw-r--r--libsolidity/formal/Why3Translator.cpp9
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});
}