Import further Clang-defined ia32 builtins

Imported using `clang_builtins.py` and filtered to make sure the
declarations aren't present in one of the existing files.

Author: tautschnig

src/ansi-c/CMakeLists.txt

@@ -65,6 +65,7 @@ make_inc(compiler_headers/gcc_builtin_headers_ia32-2)
 make_inc(compiler_headers/gcc_builtin_headers_ia32-3)
 make_inc(compiler_headers/gcc_builtin_headers_ia32-4)
 make_inc(compiler_headers/gcc_builtin_headers_ia32-5)
+make_inc(compiler_headers/gcc_builtin_headers_ia32-6)
 make_inc(compiler_headers/gcc_builtin_headers_math)
 make_inc(compiler_headers/gcc_builtin_headers_mem_string)
 make_inc(compiler_headers/gcc_builtin_headers_mips)
@@ -88,6 +89,7 @@ set(extra_dependencies
     ${CMAKE_CURRENT_BINARY_DIR}/compiler_headers/gcc_builtin_headers_ia32-3.inc
     ${CMAKE_CURRENT_BINARY_DIR}/compiler_headers/gcc_builtin_headers_ia32-4.inc
     ${CMAKE_CURRENT_BINARY_DIR}/compiler_headers/gcc_builtin_headers_ia32-5.inc
+    ${CMAKE_CURRENT_BINARY_DIR}/compiler_headers/gcc_builtin_headers_ia32-6.inc
     ${CMAKE_CURRENT_BINARY_DIR}/compiler_headers/gcc_builtin_headers_ia32.inc
     ${CMAKE_CURRENT_BINARY_DIR}/compiler_headers/gcc_builtin_headers_math.inc
     ${CMAKE_CURRENT_BINARY_DIR}/compiler_headers/gcc_builtin_headers_mem_string.inc

src/ansi-c/Makefile

@@ -60,6 +60,7 @@ BUILTIN_FILES = \
   compiler_headers/gcc_builtin_headers_ia32-3.inc \
   compiler_headers/gcc_builtin_headers_ia32-4.inc \
   compiler_headers/gcc_builtin_headers_ia32-5.inc \
+  compiler_headers/gcc_builtin_headers_ia32-6.inc \
   compiler_headers/gcc_builtin_headers_ia32.inc \
   compiler_headers/gcc_builtin_headers_math.inc \
   compiler_headers/gcc_builtin_headers_mem_string.inc \

src/ansi-c/ansi_c_internal_additions.cpp

@@ -73,6 +73,9 @@ const char gcc_builtin_headers_ia32_4[] =
 const char gcc_builtin_headers_ia32_5[] =
 #include "compiler_headers/gcc_builtin_headers_ia32-5.inc" // IWYU pragma: keep
   ; // NOLINT(whitespace/semicolon)
+const char gcc_builtin_headers_ia32_6[] =
+#include "compiler_headers/gcc_builtin_headers_ia32-6.inc" // IWYU pragma: keep
+  ; // NOLINT(whitespace/semicolon)
 
 const char gcc_builtin_headers_alpha[] =
   "#line 1 \"gcc_builtin_headers_alpha.h\"\n"

src/ansi-c/ansi_c_internal_additions.h

@@ -30,6 +30,7 @@ extern const char gcc_builtin_headers_ia32_2[];
 extern const char gcc_builtin_headers_ia32_3[];
 extern const char gcc_builtin_headers_ia32_4[];
 extern const char gcc_builtin_headers_ia32_5[];
+extern const char gcc_builtin_headers_ia32_6[];
 extern const char gcc_builtin_headers_alpha[];
 extern const char gcc_builtin_headers_arm[];
 extern const char gcc_builtin_headers_mips[];

src/ansi-c/builtin_factory.cpp

@@ -179,6 +179,9 @@ bool builtin_factory(
 
       if(find_pattern(pattern, gcc_builtin_headers_ia32_5, s))
         return convert(identifier, s, symbol_table, mh);
+
+      if(find_pattern(pattern, gcc_builtin_headers_ia32_6, s))
+        return convert(identifier, s, symbol_table, mh);
     }
     else if(config.ansi_c.arch=="arm64" ||
             config.ansi_c.arch=="armel" ||

src/ansi-c/compiler_headers/clang_builtins.py

@@ -43,7 +43,7 @@
         'v': 'void',
         'w': 'wchar_t',
         'x': '_Float16',
-        'y': '__bf16',
+        'y': '_Float16', # would be '__bf16', but we don't support that yet
         'z': '__CPROVER_size_t'
         }
 
@@ -209,7 +209,7 @@ def process_line(name, types, attributes):
     i = 0
     while i < len(types):
         (t, i_updated) = build_type(types, i)
-        assert i_updated > i, ('failed to parse type spec of' + name + ': ' +
+        assert i_updated > i, ('failed to parse type spec of ' + name + ': ' +
                                types[i:])
         i = i_updated
         type_specs.append(t)