Merge pull request #2628 from diffblue/clang-extensions

ansi-c: clang extensions

Author: kroening

regression/ansi-c/gcc_float_types1/main.c

@@ -0,0 +1,19 @@
+// for gcc, __float80 and __float128 are typedefs
+// for clang, __float128 is a keyword, and __float80 doesn't exist.
+
+#ifdef __clang__
+int __float80;
+__float128 f128;
+#else
+__float80 f80;
+__float128 f128;
+#endif
+
+int main()
+{
+  #ifndef __clang__
+  // on gcc, they can be re-declared, as they are identifiers, not keywords
+  int __float80;
+  int __float128;
+  #endif
+}

regression/ansi-c/gcc_float_types1/test.desc

@@ -0,0 +1,8 @@
+CORE gcc-only
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+^CONVERSION ERROR$

src/ansi-c/ansi_c_declaration.cpp

@@ -150,9 +150,10 @@ void ansi_c_declarationt::to_symbol(
     if(get_is_inline())
       symbol.type.set(ID_C_inlined, true);
 
-    if(config.ansi_c.mode==configt::ansi_ct::flavourt::GCC ||
-       config.ansi_c.mode==configt::ansi_ct::flavourt::APPLE ||
-       config.ansi_c.mode==configt::ansi_ct::flavourt::ARM)
+    if(
+      config.ansi_c.mode == configt::ansi_ct::flavourt::GCC ||
+      config.ansi_c.mode == configt::ansi_ct::flavourt::CLANG ||
+      config.ansi_c.mode == configt::ansi_ct::flavourt::ARM)
     {
       // GCC extern inline cleanup, to enable remove_internal_symbols
       // do its full job

src/ansi-c/ansi_c_internal_additions.cpp

@@ -182,21 +182,45 @@ void ansi_c_internal_additions(std::string &code)
     "\n";
 
   // GCC junk stuff, also for CLANG and ARM
-  if(config.ansi_c.mode==configt::ansi_ct::flavourt::GCC ||
-     config.ansi_c.mode==configt::ansi_ct::flavourt::APPLE ||
-     config.ansi_c.mode==configt::ansi_ct::flavourt::ARM)
+  if(
+    config.ansi_c.mode == configt::ansi_ct::flavourt::GCC ||
+    config.ansi_c.mode == configt::ansi_ct::flavourt::CLANG ||
+    config.ansi_c.mode == configt::ansi_ct::flavourt::ARM)
   {
     code+=gcc_builtin_headers_types;
 
     // there are many more, e.g., look at
     // https://developer.apple.com/library/mac/#documentation/developertools/gcc-4.0.1/gcc/Target-Builtins.html
 
-    if(config.ansi_c.arch=="i386" ||
-       config.ansi_c.arch=="x86_64" ||
-       config.ansi_c.arch=="x32")
+    if(
+      config.ansi_c.arch == "i386" || config.ansi_c.arch == "x86_64" ||
+      config.ansi_c.arch == "x32" || config.ansi_c.arch == "powerpc" ||
+      config.ansi_c.arch == "ppc64" || config.ansi_c.arch == "ppc64le" ||
+      config.ansi_c.arch == "ia64")
     {
-      if(config.ansi_c.mode==configt::ansi_ct::flavourt::APPLE)
-        code+="typedef double __float128;\n"; // clang doesn't do __float128
+      // https://gcc.gnu.org/onlinedocs/gcc/Floating-Types.html
+      // For clang, __float128 is a keyword.
+      // For gcc, this is a typedef and not a keyword.
+      if(config.ansi_c.mode != configt::ansi_ct::flavourt::CLANG)
+        code += "typedef __CPROVER_Float128 __float128;\n";
+    }
+    else if(config.ansi_c.arch == "hppa")
+    {
+      // https://gcc.gnu.org/onlinedocs/gcc/Floating-Types.html
+      // For clang, __float128 is a keyword.
+      // For gcc, this is a typedef and not a keyword.
+      if(config.ansi_c.mode != configt::ansi_ct::flavourt::CLANG)
+        code+="typedef long double __float128;\n";
+    }
+
+    if(
+      config.ansi_c.arch == "i386" || config.ansi_c.arch == "x86_64" ||
+      config.ansi_c.arch == "x32" || config.ansi_c.arch == "ia64")
+    {
+      // clang doesn't do __float80
+      // Note that __float80 is a typedef, and not a keyword.
+      if(config.ansi_c.mode != configt::ansi_ct::flavourt::CLANG)
+        code += "typedef __CPROVER_Float64x __float80;\n";
     }
 
     // On 64-bit systems, gcc has typedefs

src/ansi-c/builtin_factory.cpp

@@ -134,9 +134,10 @@ bool builtin_factory(
   }
 
   // GCC junk stuff, also for CLANG and ARM
-  if(config.ansi_c.mode==configt::ansi_ct::flavourt::GCC ||
-     config.ansi_c.mode==configt::ansi_ct::flavourt::APPLE ||
-     config.ansi_c.mode==configt::ansi_ct::flavourt::ARM)
+  if(
+    config.ansi_c.mode == configt::ansi_ct::flavourt::GCC ||
+    config.ansi_c.mode == configt::ansi_ct::flavourt::CLANG ||
+    config.ansi_c.mode == configt::ansi_ct::flavourt::ARM)
   {
     if(find_pattern(pattern, gcc_builtin_headers_generic, s))
       return convert(identifier, s, symbol_table, mh);

src/ansi-c/c_typecheck_base.cpp

@@ -336,7 +336,7 @@ void c_typecheck_baset::typecheck_redefinition_non_type(
         if(
           old_symbol.type.get_bool(ID_C_inlined) &&
           (config.ansi_c.mode == configt::ansi_ct::flavourt::GCC ||
-           config.ansi_c.mode == configt::ansi_ct::flavourt::APPLE ||
+           config.ansi_c.mode == configt::ansi_ct::flavourt::CLANG ||
            config.ansi_c.mode == configt::ansi_ct::flavourt::ARM ||
            config.ansi_c.mode == configt::ansi_ct::flavourt::VISUAL_STUDIO))
         {

src/ansi-c/gcc_builtin_headers_ia32.h

@@ -1,11 +1,11 @@
 // from
 // http://gcc.gnu.org/onlinedocs/gcc-4.7.0/gcc/X86-Built_002din-Functions.html
 
-__float128 __builtin_fabsq(__float128);
-__float128 __builtin_copysignq(__float128, __float128);
+__CPROVER_Float128 __builtin_fabsq(__CPROVER_Float128);
+__CPROVER_Float128 __builtin_copysignq(__CPROVER_Float128, __CPROVER_Float128);
 void __builtin_ia32_pause();
-__float128 __builtin_infq(void);
-__float128 __builtin_huge_valq(void);
+__CPROVER_Float128 __builtin_infq(void);
+__CPROVER_Float128 __builtin_huge_valq(void);
 __gcc_v8qi __builtin_ia32_paddb(__gcc_v8qi, __gcc_v8qi);
 __gcc_v4hi __builtin_ia32_paddw(__gcc_v4hi, __gcc_v4hi);
 __gcc_v2si __builtin_ia32_paddd(__gcc_v2si, __gcc_v2si);

src/ansi-c/get-gcc-builtins.sh

@@ -102,7 +102,7 @@ cat > builtins.h <<EOF
 // some newer versions of GCC apparently support __floatXYZ
 #define dfloat32_type_node __float32
 #define dfloat64_type_node __float64
-#define dfloat128_type_node __float128
+#define dfloat128_type_node __CPROVER_Float128
 
 #define build_qualified_type(t, q) q t
 #define build_pointer_type(t) t*