Tacas fixes

Author: keram88

include/smack/Naming.h

@@ -33,6 +33,7 @@ class Naming {
   static const std::string FLOAT_TYPE;
   static const std::string DOUBLE_TYPE;
   static const std::string LONG_DOUBLE_TYPE;
+  static const std::string FP128_TYPE;
   static const std::string PTR_TYPE;
   static const std::string VECTOR_TYPE;
   static const std::string NULL_VAL;

lib/smack/Prelude.cpp

@@ -178,9 +178,9 @@ const std::vector<unsigned> IntOpGen::INTEGER_SIZES{
 // floating-point layout map: bit-width -> (exponent bit-width, significand
 // bit-width)
 const std::map<unsigned, std::pair<unsigned, unsigned>> FpOpGen::FP_LAYOUT{
-    {16, {5, 11}}, {32, {8, 24}}, {64, {11, 53}}, {80, {15, 65}}};
+    {16, {5, 11}}, {32, {8, 24}}, {64, {11, 53}}, {80, {15, 65}}, {128 , {15, 113}}};
 
-const std::vector<unsigned> FpOpGen::FP_BIT_WIDTHS{16, 32, 64, 80};
+const std::vector<unsigned> FpOpGen::FP_BIT_WIDTHS{16, 32, 64, 80, 128};
 
 // make Boogie map selection expression such as
 // M[p], M[$add.ref(p, 1)]

lib/smack/SmackRep.cpp

@@ -226,6 +226,8 @@ std::string SmackRep::type(const llvm::Type *t) {
       return Naming::DOUBLE_TYPE;
     else if (t->isX86_FP80Ty())
       return Naming::LONG_DOUBLE_TYPE;
+    else if (t->isFP128Ty())
+      return Naming::FP128_TYPE;
     else
       llvm_unreachable("Unsupported floating-point type.");
   }