Kmeakin opened PR #6037 from icmp-numeric-limits
to main
:
Adds the following rewrites:
;; ult(x, 0) == false. ;; ule(x, 0) == eq(x, 0) ;; ugt(x, 0) == ne(x, 0). ;; uge(x, 0) == true. ;; ult(x, UMAX) == ne(x, UMAX). ;; ule(x, UMAX) == true. ;; ugt(x, UMAX) == false. ;; uge(x, UMAX) == eq(x, UMAX). ;; slt(x, SMIN) == false. ;; sle(x, SMIN) == eq(x, SMIN). ;; sgt(x, SMIN) == ne(x, SMIN). ;; sge(x, SMIN) == true. ;; slt(x, SMAX) == ne(x, SMAX). ;; sle(x, SMAX) == true. ;; sgt(x, SMAX) == false. ;; sge(x, SMAX) == eq(x, SMAX).
Also adds
ty_umin
,ty_umax
,ty_smin
andty_smax
constructors
cfallin assigned PR #6037 to cfallin.
cfallin submitted PR review.
Kmeakin updated PR #6037 (assigned to cfallin) from icmp-numeric-limits
to main
.
Kmeakin requested cfallin for a review on PR #6037.
cfallin submitted PR review.
cfallin merged PR #6037.
Last updated: Nov 22 2024 at 16:03 UTC