aboutsummaryrefslogtreecommitdiff
path: root/src/CStringification.v
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2019-01-14 20:09:21 -0500
committerGravatar Jason Gross <jasongross9@gmail.com>2019-01-15 14:00:52 -0500
commit456cffcd2e808a3a9c3ff47f988138bbce555e0e (patch)
tree1ad646e6b3a65ae30e5e02fe09c0e64cb04affb8 /src/CStringification.v
parentc61d5be86e3efb978883fc60687af42192aacaff (diff)
Fix computation of INTX_MIN
The minimum is -2^(bitwidth-1), not -2^bitwidth. Oops.
Diffstat (limited to 'src/CStringification.v')
-rw-r--r--src/CStringification.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/CStringification.v b/src/CStringification.v
index 2321d3a3d..b61421bc4 100644
--- a/src/CStringification.v
+++ b/src/CStringification.v
@@ -616,7 +616,7 @@ Module Compilers.
Definition to_zrange (t : type) : zrange
:= let bw := bitwidth_of t in
if is_signed t
- then r[-2^bw ~> 2^(bw-1) - 1]
+ then r[-2^(bw-1) ~> 2^(bw-1) - 1]
else r[0 ~> 2^bw - 1].
Definition is_tighter_than (t1 t2 : type)
:= ZRange.is_tighter_than_bool (to_zrange t1) (to_zrange t2).