the c_types now have stronger C++ types

Author: Daniel Kroening

src/ansi-c/ansi_c_convert_type.cpp

@@ -464,14 +464,25 @@ void ansi_c_convert_typet::write(typet &type)
       }
 
       if(int8_cnt)
-        type=is_signed?signed_char_type():unsigned_char_type();
+        if(is_signed)
+          type=signed_char_type();
+        else
+          type=unsigned_char_type();
       else if(int16_cnt)
-        type=is_signed?signed_short_int_type():unsigned_short_int_type();
+        if(is_signed)
+          type=signed_short_int_type();
+        else
+          type=unsigned_short_int_type();
       else if(int32_cnt)
-        type=is_signed?signed_int_type():unsigned_int_type();
+        if(is_signed)
+          type=signed_int_type();
+        else
+          type=unsigned_int_type();
       else if(int64_cnt) // Visual Studio: equivalent to long long int
-        type=
-          is_signed?signed_long_long_int_type():unsigned_long_long_int_type();
+        if(is_signed)
+          type=signed_long_long_int_type();
+        else
+          type=unsigned_long_long_int_type();
       else
         assert(false);
     }
@@ -509,19 +520,31 @@ void ansi_c_convert_typet::write(typet &type)
         throw 0;
       }
 
-      type=is_signed?signed_short_int_type():unsigned_short_int_type();
+      if(is_signed)
+        type=signed_short_int_type();
+      else
+        type=unsigned_short_int_type();
     }
     else if(long_cnt==0)
     {
-      type=is_signed?signed_int_type():unsigned_int_type();
+      if(is_signed)
+        type=signed_int_type();
+      else
+        type=unsigned_int_type();
     }
     else if(long_cnt==1)
     {
-      type=is_signed?signed_long_int_type():unsigned_long_int_type();
+      if(is_signed)
+        type=signed_long_int_type();
+      else
+        type=unsigned_long_int_type();
     }
     else if(long_cnt==2)
     {
-      type=is_signed?signed_long_long_int_type():unsigned_long_long_int_type();
+      if(is_signed)
+        type=signed_long_long_int_type();
+      else
+        type=unsigned_long_long_int_type();
     }
     else
     {

src/ansi-c/c_typecheck_type.cpp

@@ -134,39 +134,74 @@ void c_typecheck_baset::typecheck_type(typet &type)
       typet result;
 
       if(mode=="__QI__") // 8 bits
-        result=is_signed?signed_char_type():unsigned_char_type();
+        if(is_signed)
+          result=signed_char_type();
+        else
+          result=unsigned_char_type();
       else if(mode=="__byte__") // 8 bits
-        result=is_signed?signed_char_type():unsigned_char_type();
+        if(is_signed)
+          result=signed_char_type();
+        else
+          result=unsigned_char_type();
       else if(mode=="__HI__") // 16 bits
-        result=is_signed?signed_short_int_type():unsigned_short_int_type();
+        if(is_signed)
+          result=signed_short_int_type();
+        else
+          result=unsigned_short_int_type();
       else if(mode=="__SI__") // 32 bits
-        result=is_signed?signed_int_type():unsigned_int_type();
+        if(is_signed)
+          result=signed_int_type();
+        else
+          result=unsigned_int_type();
       else if(mode=="__word__") // long int, we think
-        result=is_signed?signed_long_int_type():unsigned_long_int_type();
+        if(is_signed)
+          result=signed_long_int_type();
+        else
+          result=unsigned_long_int_type();
       else if(mode=="__pointer__") // we think this is size_t/ssize_t
-        result=is_signed?signed_size_type():size_type();
+        if(is_signed)
+          result=signed_size_type();
+        else
+          result=size_type();
       else if(mode=="__DI__") // 64 bits
       {
         if(config.ansi_c.long_int_width==64)
-          result=is_signed?signed_long_int_type():unsigned_long_int_type();
+          if(is_signed)
+            result=signed_long_int_type();
+          else
+            result=unsigned_long_int_type();
         else
         {
           assert(config.ansi_c.long_long_int_width==64);
-          result=
-            is_signed?signed_long_long_int_type():unsigned_long_long_int_type();
+
+          if(is_signed)
+            result=signed_long_long_int_type();
+          else
+            result=unsigned_long_long_int_type();
         }
       }
       else if(mode=="__TI__") // 128 bits
-        result=is_signed?gcc_signed_int128_type():gcc_unsigned_int128_type();
+        if(is_signed)
+          result=gcc_signed_int128_type();
+        else
+          result=gcc_unsigned_int128_type();
       else if(mode=="__V2SI__") // vector of 2 ints, deprecated by gcc
-        result=
-          vector_typet(
-            is_signed?signed_int_type():unsigned_int_type(),
+        if(is_signed)
+          result=vector_typet(
+            signed_int_type(),
+            from_integer(2, size_type()));
+        else
+          result=vector_typet(
+            unsigned_int_type(),
             from_integer(2, size_type()));
       else if(mode=="__V4SI__") // vector of 4 ints, deprecated by gcc
-        result=
-          vector_typet(
-            is_signed?signed_int_type():unsigned_int_type(),
+        if(is_signed)
+          result=vector_typet(
+            signed_int_type(),
+            from_integer(4, size_type()));
+        else
+          result=vector_typet(
+            unsigned_int_type(),
             from_integer(4, size_type()));
       else // give up, just use subtype
         result=type.subtype();

src/util/c_types.cpp

@@ -23,7 +23,7 @@ Function: index_type
 
 \*******************************************************************/
 
-typet index_type()
+bitvector_typet index_type()
 {
   // same as signed size type
   return signed_size_type();
@@ -41,7 +41,7 @@ Function: enum_constant_type
 
 \*******************************************************************/
 
-typet enum_constant_type()
+bitvector_typet enum_constant_type()
 {
   // usually same as 'int',
   // but might be unsigned, or shorter than 'int'
@@ -60,9 +60,9 @@ Function: signed_int_type
 
 \*******************************************************************/
 
-typet signed_int_type()
+signedbv_typet signed_int_type()
 {
-  typet result=signedbv_typet(config.ansi_c.int_width);
+  signedbv_typet result(config.ansi_c.int_width);
   result.set(ID_C_c_type, ID_signed_int);
   return result;
 }
@@ -79,9 +79,9 @@ Function: signed_short_int_type
 
 \*******************************************************************/
 
-typet signed_short_int_type()
+signedbv_typet signed_short_int_type()
 {
-  typet result=signedbv_typet(config.ansi_c.short_int_width);
+  signedbv_typet result(config.ansi_c.short_int_width);
   result.set(ID_C_c_type, ID_signed_short_int);
   return result;
 }
@@ -98,9 +98,9 @@ Function: unsigned_int_type
 
 \*******************************************************************/
 
-typet unsigned_int_type()
+unsignedbv_typet unsigned_int_type()
 {
-  typet result=unsignedbv_typet(config.ansi_c.int_width);
+  unsignedbv_typet result(config.ansi_c.int_width);
   result.set(ID_C_c_type, ID_unsigned_int);
   return result;
 }
@@ -117,9 +117,9 @@ Function: unsigned_short_int_type
 
 \*******************************************************************/
 
-typet unsigned_short_int_type()
+unsignedbv_typet unsigned_short_int_type()
 {
-  typet result=unsignedbv_typet(config.ansi_c.short_int_width);
+  unsignedbv_typet result(config.ansi_c.short_int_width);
   result.set(ID_C_c_type, ID_unsigned_short_int);
   return result;
 }
@@ -136,7 +136,7 @@ Function: size_type
 
 \*******************************************************************/
 
-typet size_type()
+unsignedbv_typet size_type()
 {
   // The size type varies. This is unsigned int on some systems,
   // and unsigned long int on others,
@@ -164,7 +164,7 @@ Function: signed_size_type
 
 \*******************************************************************/
 
-typet signed_size_type()
+signedbv_typet signed_size_type()
 {
   // we presume this is the same as pointer difference
   return pointer_diff_type();
@@ -182,9 +182,9 @@ Function: signed_long_int_type
 
 \*******************************************************************/
 
-typet signed_long_int_type()
+signedbv_typet signed_long_int_type()
 {
-  typet result=signedbv_typet(config.ansi_c.long_int_width);
+  signedbv_typet result(config.ansi_c.long_int_width);
   result.set(ID_C_c_type, ID_signed_long_int);
   return result;
 }
@@ -201,9 +201,9 @@ Function: signed_long_long_int_type
 
 \*******************************************************************/
 
-typet signed_long_long_int_type()
+signedbv_typet signed_long_long_int_type()
 {
-  typet result=signedbv_typet(config.ansi_c.long_long_int_width);
+  signedbv_typet result(config.ansi_c.long_long_int_width);
   result.set(ID_C_c_type, ID_signed_long_long_int);
   return result;
 }
@@ -220,9 +220,9 @@ Function: unsigned_long_int_type
 
 \*******************************************************************/
 
-typet unsigned_long_int_type()
+unsignedbv_typet unsigned_long_int_type()
 {
-  typet result=unsignedbv_typet(config.ansi_c.long_int_width);
+  unsignedbv_typet result(config.ansi_c.long_int_width);
   result.set(ID_C_c_type, ID_unsigned_long_int);
   return result;
 }
@@ -239,9 +239,9 @@ Function: unsigned_long_long_int_type
 
 \*******************************************************************/
 
-typet unsigned_long_long_int_type()
+unsignedbv_typet unsigned_long_long_int_type()
 {
-  typet result=unsignedbv_typet(config.ansi_c.long_long_int_width);
+  unsignedbv_typet result(config.ansi_c.long_long_int_width);
   result.set(ID_C_c_type, ID_unsigned_long_long_int);
   return result;
 }
@@ -276,23 +276,25 @@ Function: char_type
 
 \*******************************************************************/
 
-typet char_type()
+bitvector_typet char_type()
 {
-  typet result;
-
   // this can be signed or unsigned, depending on the architecture
 
-  if(config.ansi_c.char_is_unsigned)
-    result=unsignedbv_typet(config.ansi_c.char_width);
-  else
-    result=signedbv_typet(config.ansi_c.char_width);
-
   // There are 3 char types, i.e., this one is
   // different from either signed char or unsigned char!
 
-  result.set(ID_C_c_type, ID_char);
-
-  return result;
+  if(config.ansi_c.char_is_unsigned)
+  {
+    unsignedbv_typet result(config.ansi_c.char_width);
+    result.set(ID_C_c_type, ID_char);
+    return result;
+  }
+  else
+  {
+    signedbv_typet result(config.ansi_c.char_width);
+    result.set(ID_C_c_type, ID_char);
+    return result;
+  }
 }
 
 /*******************************************************************\
@@ -307,12 +309,10 @@ Function: unsigned_char_type
 
 \*******************************************************************/
 
-typet unsigned_char_type()
+unsignedbv_typet unsigned_char_type()
 {
-  typet result=unsignedbv_typet(config.ansi_c.char_width);
-
+  unsignedbv_typet result(config.ansi_c.char_width);
   result.set(ID_C_c_type, ID_unsigned_char);
-
   return result;
 }
 
@@ -328,12 +328,10 @@ Function: signed_char_type
 
 \*******************************************************************/
 
-typet signed_char_type()
+signedbv_typet signed_char_type()
 {
-  typet result=signedbv_typet(config.ansi_c.char_width);
-
+  signedbv_typet result(config.ansi_c.char_width);
   result.set(ID_C_c_type, ID_signed_char);
-
   return result;
 }
 
@@ -349,18 +347,20 @@ Function: wchar_t_type
 
 \*******************************************************************/
 
-typet wchar_t_type()
+bitvector_typet wchar_t_type()
 {
-  typet result;
-
   if(config.ansi_c.wchar_t_is_unsigned)
-    result=unsignedbv_typet(config.ansi_c.wchar_t_width);
+  {
+    unsignedbv_typet result(config.ansi_c.wchar_t_width);
+    result.set(ID_C_c_type, ID_wchar_t);
+    return result;
+  }
   else
-    result=signedbv_typet(config.ansi_c.wchar_t_width);
-
-  result.set(ID_C_c_type, ID_wchar_t);
-
-  return result;
+  {
+    signedbv_typet result(config.ansi_c.wchar_t_width);
+    result.set(ID_C_c_type, ID_wchar_t);
+    return result;
+  }
 }
 
 /*******************************************************************\
@@ -375,17 +375,13 @@ Function: char16_t_type
 
 \*******************************************************************/
 
-typet char16_t_type()
+unsignedbv_typet char16_t_type()
 {
-  typet result;
-
   // Types char16_t and char32_t denote distinct types with the same size,
   // signedness, and alignment as uint_least16_t and uint_least32_t,
   // respectively, in <stdint.h>, called the underlying types.
-  result=unsignedbv_typet(16);
-
+  unsignedbv_typet result(16);
   result.set(ID_C_c_type, ID_char16_t);
-
   return result;
 }
 
@@ -401,17 +397,13 @@ Function: char32_t_type
 
 \*******************************************************************/
 
-typet char32_t_type()
+unsignedbv_typet char32_t_type()
 {
-  typet result;
-
   // Types char16_t and char32_t denote distinct types with the same size,
   // signedness, and alignment as uint_least16_t and uint_least32_t,
   // respectively, in <stdint.h>, called the underlying types.
-  result=unsignedbv_typet(32);
-
+  unsignedbv_typet result(32);
   result.set(ID_C_c_type, ID_char32_t);
-
   return result;
 }
 
@@ -427,23 +419,23 @@ Function: float_type
 
 \*******************************************************************/
 
-typet float_type()
+bitvector_typet float_type()
 {
-  typet result;
-
   if(config.ansi_c.use_fixed_for_float)
   {
-    fixedbv_typet tmp;
-    tmp.set_width(config.ansi_c.single_width);
-    tmp.set_integer_bits(config.ansi_c.single_width/2);
-    result=tmp;
+    fixedbv_typet result;
+    result.set_width(config.ansi_c.single_width);
+    result.set_integer_bits(config.ansi_c.single_width/2);
+    result.set(ID_C_c_type, ID_float);
+    return result;
   }
   else
-    result=ieee_float_spect::single_precision().to_type();
-
-  result.set(ID_C_c_type, ID_float);
-
-  return result;
+  {
+    floatbv_typet result=
+      ieee_float_spect::single_precision().to_type();
+    result.set(ID_C_c_type, ID_float);
+    return result;
+  }
 }
 
 /*******************************************************************\
@@ -458,23 +450,23 @@ Function: double_type
 
 \*******************************************************************/
 
-typet double_type()
+bitvector_typet double_type()
 {
-  typet result;
-
   if(config.ansi_c.use_fixed_for_float)
   {
-    fixedbv_typet tmp;
-    tmp.set_width(config.ansi_c.double_width);
-    tmp.set_integer_bits(config.ansi_c.double_width/2);
-    result=tmp;
+    fixedbv_typet result;
+    result.set_width(config.ansi_c.double_width);
+    result.set_integer_bits(config.ansi_c.double_width/2);
+    result.set(ID_C_c_type, ID_double);
+    return result;
   }
   else
-    result=ieee_float_spect::double_precision().to_type();
-
-  result.set(ID_C_c_type, ID_double);
-
-  return result;
+  {
+    floatbv_typet result=
+      ieee_float_spect::double_precision().to_type();
+    result.set(ID_C_c_type, ID_double);
+    return result;
+  }
 }
 
 /*******************************************************************\
@@ -489,19 +481,19 @@ Function: long_double_type
 
 \*******************************************************************/
 
-typet long_double_type()
+bitvector_typet long_double_type()
 {
-  typet result;
-
   if(config.ansi_c.use_fixed_for_float)
   {
-    fixedbv_typet tmp;
-    tmp.set_width(config.ansi_c.long_double_width);
-    tmp.set_integer_bits(config.ansi_c.long_double_width/2);
-    result=tmp;
+    fixedbv_typet result;
+    result.set_width(config.ansi_c.long_double_width);
+    result.set_integer_bits(config.ansi_c.long_double_width/2);
+    result.set(ID_C_c_type, ID_long_double);
+    return result;
   }
   else
   {
+    floatbv_typet result;
     if(config.ansi_c.long_double_width==128)
       result=ieee_float_spect::quadruple_precision().to_type();
     else if(config.ansi_c.long_double_width==64)
@@ -520,11 +512,11 @@ typet long_double_type()
     }
     else
       assert(false);
-  }
 
-  result.set(ID_C_c_type, ID_long_double);
+    result.set(ID_C_c_type, ID_long_double);
 
-  return result;
+    return result;
+  }
 }
 
 /*******************************************************************\
@@ -539,26 +531,25 @@ Function: gcc_float128_type
 
 \*******************************************************************/
 
-typet gcc_float128_type()
+bitvector_typet gcc_float128_type()
 {
-  typet result;
+  // not same as long double!
 
   if(config.ansi_c.use_fixed_for_float)
   {
-    fixedbv_typet tmp;
-    tmp.set_width(128);
-    tmp.set_integer_bits(128/2);
-    result=tmp;
+    fixedbv_typet result;
+    result.set_width(128);
+    result.set_integer_bits(128/2);
+    result.set(ID_C_c_type, ID_gcc_float128);
+    return result;
   }
   else
   {
-    result=ieee_float_spect::quadruple_precision().to_type();
+    floatbv_typet result=
+      ieee_float_spect::quadruple_precision().to_type();
+    result.set(ID_C_c_type, ID_gcc_float128);
+    return result;
   }
-
-  // not same as long double!
-  result.set(ID_C_c_type, ID_gcc_float128);
-
-  return result;
 }
 
 /*******************************************************************\
@@ -573,7 +564,7 @@ Function: pointer_diff_type
 
 \*******************************************************************/
 
-typet pointer_diff_type()
+signedbv_typet pointer_diff_type()
 {
   // The pointer-diff type varies. This is signed int on some systems,
   // and signed long int on others, and signed long long on say Windows.
@@ -600,7 +591,7 @@ Function: pointer_type
 
 \*******************************************************************/
 
-typet pointer_type(const typet &subtype)
+pointer_typet pointer_type(const typet &subtype)
 {
   return pointer_typet(subtype);
 }
@@ -617,7 +608,7 @@ Function: reference_type
 
 \*******************************************************************/
 
-typet reference_type(const typet &subtype)
+reference_typet reference_type(const typet &subtype)
 {
   return reference_typet(subtype);
 }
@@ -651,9 +642,9 @@ Function: gcc_unsigned_int128_type
 
 \*******************************************************************/
 
-typet gcc_unsigned_int128_type()
+unsignedbv_typet gcc_unsigned_int128_type()
 {
-  typet result=unsignedbv_typet(128);
+  unsignedbv_typet result(128);
   result.set(ID_C_c_type, ID_unsigned_int128);
   return result;
 }
@@ -670,9 +661,9 @@ Function: gcc_signed_int128_type
 
 \*******************************************************************/
 
-typet gcc_signed_int128_type()
+signedbv_typet gcc_signed_int128_type()
 {
-  typet result=signedbv_typet(128);
+  signedbv_typet result(128);
   result.set(ID_C_c_type, ID_signed_int128);
   return result;
 }

src/util/c_types.h

@@ -9,39 +9,39 @@ Author: Daniel Kroening, kroening@kroening.com
 #ifndef CPROVER_UTIL_C_TYPES_H
 #define CPROVER_UTIL_C_TYPES_H
 
-#include "type.h"
-
-typet index_type();
-typet enum_constant_type();
-typet signed_int_type();
-typet unsigned_int_type();
-typet signed_long_int_type();
-typet signed_short_int_type();
-typet unsigned_short_int_type();
-typet signed_long_long_int_type();
-typet unsigned_long_int_type();
-typet unsigned_long_long_int_type();
+#include "std_types.h"
+
+bitvector_typet index_type();
+bitvector_typet enum_constant_type();
+signedbv_typet signed_int_type();
+unsignedbv_typet unsigned_int_type();
+signedbv_typet signed_long_int_type();
+signedbv_typet signed_short_int_type();
+unsignedbv_typet unsigned_short_int_type();
+signedbv_typet signed_long_long_int_type();
+unsignedbv_typet unsigned_long_int_type();
+unsignedbv_typet unsigned_long_long_int_type();
 typet c_bool_type();
-typet char_type();
-typet unsigned_char_type();
-typet signed_char_type();
-typet wchar_t_type();
-typet char16_t_type();
-typet char32_t_type();
-typet float_type();
-typet double_type();
-typet long_double_type();
-typet gcc_float128_type();
-typet gcc_unsigned_int128_type();
-typet gcc_signed_int128_type();
-typet size_type();
-typet signed_size_type();
-typet pointer_diff_type();
-typet pointer_type(const typet &);
+bitvector_typet char_type();
+unsignedbv_typet unsigned_char_type();
+signedbv_typet signed_char_type();
+bitvector_typet wchar_t_type();
+unsignedbv_typet char16_t_type();
+unsignedbv_typet char32_t_type();
+bitvector_typet float_type();
+bitvector_typet double_type();
+bitvector_typet long_double_type();
+bitvector_typet gcc_float128_type();
+unsignedbv_typet gcc_unsigned_int128_type();
+signedbv_typet gcc_signed_int128_type();
+unsignedbv_typet size_type();
+signedbv_typet signed_size_type();
+signedbv_typet pointer_diff_type();
+pointer_typet pointer_type(const typet &);
 typet void_type();
 
 // This is for Java and C++
-typet reference_type(const typet &);
+reference_typet reference_type(const typet &);
 
 // Turns an ID_C_c_type into a string, e.g.,
 // ID_signed_int gets "signed int".