diff options
Diffstat (limited to 'src/AbstractInterpretation.v')
| -rw-r--r-- | src/AbstractInterpretation.v | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/src/AbstractInterpretation.v b/src/AbstractInterpretation.v index e74582ae6..0489f4dc8 100644 --- a/src/AbstractInterpretation.v +++ b/src/AbstractInterpretation.v @@ -685,6 +685,12 @@ Module Compilers. (ZRange.four_corners Z.add x y) (ZRange.eight_corners (fun x y m => Z.max 0 (x + y - m)) x y m))) + | ident.Z_combine_at_bitwidth as idc + => fun bitwidth lo hi + => bitwidth <- to_literal bitwidth; + lo <- lo; + hi <- hi; + Some (ZRange.four_corners (ident.interp idc bitwidth) lo hi) | ident.Z_cast range => fun r : option zrange => interp_Z_cast range r |