diff options
| author |  Jason Gross <jagro@google.com> | 2018-08-13 21:35:43 -0400 |
|---|---|---|
| committer | Jason Gross <jagro@google.com> | 2018-08-13 21:43:50 -0400 |
| commit | 66d064774f532066e43bbbaf27a1fa7fb3e06dfc (patch) | |
| tree | f5e64cbbe73a6cc828dc18853e085b7b39b6b82d /src/Experiments | |
| parent | e17a3a7b01fb2a61836db85daa6f7c4887635ac3 (diff) | |
Fix some bounds analysis
Diffstat (limited to 'src/Experiments')
| -rw-r--r-- | src/Experiments/NewPipeline/AbstractInterpretation.v | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/Experiments/NewPipeline/AbstractInterpretation.v b/src/Experiments/NewPipeline/AbstractInterpretation.v index bec6434a1..858832f5d 100644 --- a/src/Experiments/NewPipeline/AbstractInterpretation.v +++ b/src/Experiments/NewPipeline/AbstractInterpretation.v @@ -521,10 +521,11 @@ Module Compilers. | ident.Z_add as idc | ident.Z_mul as idc | ident.Z_sub as idc + => fun x y => x <- x; y <- y; Some (ZRange.four_corners (ident.interp idc) x y) | ident.Z_div as idc | ident.Z_shiftr as idc | ident.Z_shiftl as idc - => fun x y => x <- x; y <- y; Some (ZRange.four_corners (ident.interp idc) x y) + => fun x y => x <- x; y <- y; Some (ZRange.four_corners_and_zero (ident.interp idc) x y) | ident.Z_add_with_carry as idc => fun x y z => x <- x; y <- y; z <- z; Some (ZRange.eight_corners (ident.interp idc) x y z) | ident.Z_cc_m as idc |