From 9506b9f4add5b211a1fec4edc6cf2153b46a03f6 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 16 Aug 2018 10:06:09 -0400 Subject: Fix bounds on n_corners_and_zero I wasn't careful enough on checking 66d064774f532066e43bbbaf27a1fa7fb3e06dfc, and as a result, the bounds analysis went wrong and we generated some bad C files. This should fix that. --- src/Util/ZRange/Operations.v | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'src') diff --git a/src/Util/ZRange/Operations.v b/src/Util/ZRange/Operations.v index c8db4adf0..130fdc0c4 100644 --- a/src/Util/ZRange/Operations.v +++ b/src/Util/ZRange/Operations.v @@ -43,7 +43,7 @@ Module ZRange. := let (l, u) := eta v in r[ f l ~> f u ]. - Definition split_range_at_0 (x : zrange) : option zrange (* < 0 *) * option zrange (* = 0 *) * option zrange (* >= 0 *) + Definition split_range_at_0 (x : zrange) : option zrange (* < 0 *) * option zrange (* = 0 *) * option zrange (* > 0 *) := let (l, u) := eta x in (if (0 <=? l)%Z then None @@ -51,9 +51,9 @@ Module ZRange. if ((0 0], - if (0 <=? u)%Z - then Some r[Z.max 1 l ~> u] - else None). + if (u <=? 0)%Z + then None + else Some r[Z.max 1 l ~> u]). Definition apply_to_split_range (f : zrange -> zrange) (v : zrange) : zrange := match split_range_at_0 v with -- cgit v1.2.3