From 456cffcd2e808a3a9c3ff47f988138bbce555e0e Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 14 Jan 2019 20:09:21 -0500 Subject: Fix computation of INTX_MIN The minimum is -2^(bitwidth-1), not -2^bitwidth. Oops. --- src/CStringification.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'src/CStringification.v') 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). -- cgit v1.2.3