From 05d4047e4f8fb0ea56a5e7cbb6f384a4ce2a20f3 Mon Sep 17 00:00:00 2001
From: Daniel Dunbar <daniel@zuster.org>
Date: Fri, 12 Sep 2014 19:14:15 -0700
Subject: [FloatEvaluation] Use llvm::report_fatal_error() instead of assert(0)
 for unsupported floating point widths.

---
 include/klee/Internal/Support/FloatEvaluation.h | 33 +++++++++++++------------
 1 file 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");
   }
 }
 
-- 
cgit 1.4.1