diff options
Diffstat (limited to 'src/Experiments/NewPipeline/AbstractInterpretation.v')
| -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 |