From 08a010db3f5dac2b53c56f1ada5423e65885a9bf Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Sat, 21 Dec 2024 21:55:39 +0000 Subject: [PATCH] ieee_floatt: add preconditions This adds preconditons to further binary operators in ieee_floatt that the format must match. --- src/util/ieee_float.cpp | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/src/util/ieee_float.cpp b/src/util/ieee_float.cpp index 1fee65294a2..52a507ff958 100644 --- a/src/util/ieee_float.cpp +++ b/src/util/ieee_float.cpp @@ -915,6 +915,8 @@ ieee_floatt &ieee_floatt::operator-=(const ieee_floatt &other) bool ieee_floatt::operator<(const ieee_floatt &other) const { + PRECONDITION(other.spec == spec); + if(NaN_flag || other.NaN_flag) return false; @@ -961,6 +963,8 @@ bool ieee_floatt::operator<(const ieee_floatt &other) const bool ieee_floatt::operator<=(const ieee_floatt &other) const { + PRECONDITION(other.spec == spec); + if(NaN_flag || other.NaN_flag) return false; @@ -994,6 +998,8 @@ bool ieee_floatt::operator>=(const ieee_floatt &other) const bool ieee_floatt::operator==(const ieee_floatt &other) const { + PRECONDITION(other.spec == spec); + // packed equality! if(NaN_flag && other.NaN_flag) return true; @@ -1016,6 +1022,8 @@ bool ieee_floatt::operator==(const ieee_floatt &other) const bool ieee_floatt::ieee_equal(const ieee_floatt &other) const { + PRECONDITION(other.spec == spec); + if(NaN_flag || other.NaN_flag) return false; if(is_zero() && other.is_zero()) @@ -1038,6 +1046,8 @@ bool ieee_floatt::operator!=(const ieee_floatt &other) const bool ieee_floatt::ieee_not_equal(const ieee_floatt &other) const { + PRECONDITION(other.spec == spec); + if(NaN_flag || other.NaN_flag) return true; // !!! if(is_zero() && other.is_zero())