diff options
author | Daniel Dunbar <daniel@zuster.org> | 2014-09-12 19:14:15 -0700 |
---|---|---|
committer | Daniel Dunbar <daniel@zuster.org> | 2014-09-12 19:14:15 -0700 |
commit | 05d4047e4f8fb0ea56a5e7cbb6f384a4ce2a20f3 (patch) | |
tree | caf2b12837e456d6b3338733571b6045395a2280 | |
parent | 853cc1f5c47781cc3e3681351ffe7a6d0dcd39de (diff) | |
download | klee-05d4047e4f8fb0ea56a5e7cbb6f384a4ce2a20f3.tar.gz |
[FloatEvaluation] Use llvm::report_fatal_error() instead of assert(0) for unsupported floating point widths.
-rw-r--r-- | include/klee/Internal/Support/FloatEvaluation.h | 33 |
1 files changed, 17 insertions, 16 deletions
diff --git a/include/klee/Internal/Support/FloatEvaluation.h b/include/klee/Internal/Support/FloatEvaluation.h index f1f16c5e..6d9092f2 100644 --- a/include/klee/Internal/Support/FloatEvaluation.h +++ b/include/klee/Internal/Support/FloatEvaluation.h @@ -15,6 +15,7 @@ #include "klee/util/Bits.h" //bits64::truncateToNBits #include "IntEvaluation.h" //ints::sext +#include "llvm/Support/ErrorHandling.h" #include "llvm/Support/MathExtras.h" #include <cassert> @@ -83,7 +84,7 @@ inline uint64_t add(uint64_t l, uint64_t r, unsigned inWidth) { switch( inWidth ) { case FLT_BITS: return bits64::truncateToNBits(FloatAsUInt64(UInt64AsFloat(l) + UInt64AsFloat(r)), FLT_BITS); case DBL_BITS: return bits64::truncateToNBits(DoubleAsUInt64(UInt64AsDouble(l) + UInt64AsDouble(r)), DBL_BITS); - default: assert(0 && "invalid floating point width"); + default: llvm::report_fatal_error("unsupported floating point width"); } } @@ -92,7 +93,7 @@ inline uint64_t sub(uint64_t l, uint64_t r, unsigned inWidth) { switch( inWidth ) { case FLT_BITS: return bits64::truncateToNBits(FloatAsUInt64(UInt64AsFloat(l) - UInt64AsFloat(r)), FLT_BITS); case DBL_BITS: return bits64::truncateToNBits(DoubleAsUInt64(UInt64AsDouble(l) - UInt64AsDouble(r)), DBL_BITS); - default: assert(0 && "invalid floating point width"); + default: llvm::report_fatal_error("unsupported floating point width"); } } @@ -101,7 +102,7 @@ inline uint64_t mul(uint64_t l, uint64_t r, unsigned inWidth) { switch( inWidth ) { case FLT_BITS: return bits64::truncateToNBits(FloatAsUInt64(UInt64AsFloat(l) * UInt64AsFloat(r)), FLT_BITS); case DBL_BITS: return bits64::truncateToNBits(DoubleAsUInt64(UInt64AsDouble(l) * UInt64AsDouble(r)), DBL_BITS); - default: assert(0 && "invalid floating point width"); + default: llvm::report_fatal_error("unsupported floating point width"); } } @@ -110,7 +111,7 @@ inline uint64_t div(uint64_t l, uint64_t r, unsigned inWidth) { switch( inWidth ) { case FLT_BITS: return bits64::truncateToNBits(FloatAsUInt64(UInt64AsFloat(l) / UInt64AsFloat(r)), FLT_BITS); case DBL_BITS: return bits64::truncateToNBits(DoubleAsUInt64(UInt64AsDouble(l) / UInt64AsDouble(r)), DBL_BITS); - default: assert(0 && "invalid floating point width"); + default: llvm::report_fatal_error("unsupported floating point width"); } } @@ -119,7 +120,7 @@ inline uint64_t mod(uint64_t l, uint64_t r, unsigned inWidth) { switch( inWidth ) { case FLT_BITS: return bits64::truncateToNBits(FloatAsUInt64( fmod(UInt64AsFloat(l), UInt64AsFloat(r)) ), FLT_BITS); case DBL_BITS: return bits64::truncateToNBits(DoubleAsUInt64( fmod(UInt64AsDouble(l), UInt64AsDouble(r)) ), DBL_BITS); - default: assert(0 && "invalid floating point width"); + default: llvm::report_fatal_error("unsupported floating point width"); } } @@ -133,7 +134,7 @@ inline bool isNaN(uint64_t l, unsigned inWidth) { switch( inWidth ) { case FLT_BITS: return llvm::IsNAN( UInt64AsFloat(l) ); case DBL_BITS: return llvm::IsNAN( UInt64AsDouble(l) ); - default: assert(0 && "invalid floating point width"); + default: llvm::report_fatal_error("unsupported floating point width"); } } @@ -141,7 +142,7 @@ inline uint64_t eq(uint64_t l, uint64_t r, unsigned inWidth) { switch( inWidth ) { case FLT_BITS: return UInt64AsFloat(l) == UInt64AsFloat(r); case DBL_BITS: return UInt64AsDouble(l) == UInt64AsDouble(r); - default: assert(0 && "invalid floating point width"); + default: llvm::report_fatal_error("unsupported floating point width"); } } @@ -149,7 +150,7 @@ inline uint64_t ne(uint64_t l, uint64_t r, unsigned inWidth) { switch( inWidth ) { case FLT_BITS: return UInt64AsFloat(l) != UInt64AsFloat(r); case DBL_BITS: return UInt64AsDouble(l) != UInt64AsDouble(r); - default: assert(0 && "invalid floating point width"); + default: llvm::report_fatal_error("unsupported floating point width"); } } @@ -157,7 +158,7 @@ inline uint64_t lt(uint64_t l, uint64_t r, unsigned inWidth) { switch( inWidth ) { case FLT_BITS: return UInt64AsFloat(l) < UInt64AsFloat(r); case DBL_BITS: return UInt64AsDouble(l) < UInt64AsDouble(r); - default: assert(0 && "invalid floating point width"); + default: llvm::report_fatal_error("unsupported floating point width"); } } @@ -165,7 +166,7 @@ inline uint64_t le(uint64_t l, uint64_t r, unsigned inWidth) { switch( inWidth ) { case FLT_BITS: return UInt64AsFloat(l) <= UInt64AsFloat(r); case DBL_BITS: return UInt64AsDouble(l) <= UInt64AsDouble(r); - default: assert(0 && "invalid floating point width"); + default: llvm::report_fatal_error("unsupported floating point width"); } } @@ -173,7 +174,7 @@ inline uint64_t gt(uint64_t l, uint64_t r, unsigned inWidth) { switch( inWidth ) { case FLT_BITS: return UInt64AsFloat(l) > UInt64AsFloat(r); case DBL_BITS: return UInt64AsDouble(l) > UInt64AsDouble(r); - default: assert(0 && "invalid floating point width"); + default: llvm::report_fatal_error("unsupported floating point width"); } } @@ -181,7 +182,7 @@ inline uint64_t ge(uint64_t l, uint64_t r, unsigned inWidth) { switch( inWidth ) { case FLT_BITS: return UInt64AsFloat(l) >= UInt64AsFloat(r); case DBL_BITS: return UInt64AsDouble(l) >= UInt64AsDouble(r); - default: assert(0 && "invalid floating point width"); + default: llvm::report_fatal_error("unsupported floating point width"); } } @@ -223,7 +224,7 @@ inline uint64_t toUnsignedInt( uint64_t l, unsigned outWidth, unsigned inWidth ) switch( inWidth ) { case FLT_BITS: return bits64::truncateToNBits((uint64_t)UInt64AsFloat(l), outWidth ); case DBL_BITS: return bits64::truncateToNBits((uint64_t)UInt64AsDouble(l), outWidth ); - default: assert(0 && "invalid floating point width"); + default: llvm::report_fatal_error("unsupported floating point width"); } } @@ -232,7 +233,7 @@ inline uint64_t toSignedInt( uint64_t l, unsigned outWidth, unsigned inWidth ) { switch( inWidth ) { case FLT_BITS: return bits64::truncateToNBits((int64_t)UInt64AsFloat(l), outWidth); case DBL_BITS: return bits64::truncateToNBits((int64_t)UInt64AsDouble(l), outWidth); - default: assert(0 && "invalid floating point width"); + default: llvm::report_fatal_error("unsupported floating point width"); } } @@ -241,7 +242,7 @@ inline uint64_t UnsignedIntToFP( uint64_t l, unsigned outWidth ) { switch( outWidth ) { case FLT_BITS: return bits64::truncateToNBits(FloatAsUInt64((float)l), outWidth); case DBL_BITS: return bits64::truncateToNBits(DoubleAsUInt64((double)l), outWidth); - default: assert(0 && "invalid floating point width"); + default: llvm::report_fatal_error("unsupported floating point width"); } } @@ -250,7 +251,7 @@ inline uint64_t SignedIntToFP( uint64_t l, unsigned outWidth, unsigned inWidth ) switch( outWidth ) { case FLT_BITS: return bits64::truncateToNBits(FloatAsUInt64((float)(int64_t)ints::sext(l, 64, inWidth)), outWidth); case DBL_BITS: return bits64::truncateToNBits(DoubleAsUInt64((double)(int64_t)ints::sext(l,64, inWidth)), outWidth); - default: assert(0 && "invalid floating point width"); + default: llvm::report_fatal_error("unsupported floating point width"); } } |