diff options
| author |  Jason Gross <jgross@mit.edu> | 2018-08-16 10:06:09 -0400 |
|---|---|---|
| committer |  Jason Gross <jasongross9@gmail.com> | 2018-08-16 10:40:35 -0400 |
| commit | 9506b9f4add5b211a1fec4edc6cf2153b46a03f6 (patch) | |
| tree | 8d13dc462d0482f47d12e32b6e0f9a9e09053a63 /src | |
| parent | 8926b3f6b2aa1fe0f8d3f65f1966f60402cad4b9 (diff) | |
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.
Diffstat (limited to 'src')
| -rw-r--r-- | src/Util/ZRange/Operations.v | 8 |
1 files changed, 4 insertions, 4 deletions
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 <? l)%Z || (u <? 0)%Z)%bool then None else Some r[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 |