Added further ia32 GCC built-ins

Author: tautschnig

.gitignore

@@ -28,6 +28,8 @@ src/ansi-c/gcc_builtin_headers_alpha.inc
 src/ansi-c/gcc_builtin_headers_arm.inc
 src/ansi-c/gcc_builtin_headers_generic.inc
 src/ansi-c/gcc_builtin_headers_ia32-2.inc
+src/ansi-c/gcc_builtin_headers_ia32-3.inc
+src/ansi-c/gcc_builtin_headers_ia32-4.inc
 src/ansi-c/gcc_builtin_headers_ia32.inc
 src/ansi-c/gcc_builtin_headers_math.inc
 src/ansi-c/gcc_builtin_headers_mem_string.inc

src/ansi-c/Makefile

@@ -58,7 +58,8 @@ CLEANFILES = ansi-c$(LIBEXT) \
 	clang_builtin_headers.inc gcc_builtin_headers_ia32-2.inc \
   gcc_builtin_headers_math.inc gcc_builtin_headers_omp.inc \
   gcc_builtin_headers_tm.inc gcc_builtin_headers_ubsan.inc \
-  gcc_builtin_headers_mem_string.inc
+  gcc_builtin_headers_mem_string.inc \
+  gcc_builtin_headers_ia32-3.inc gcc_builtin_headers_ia32-4.inc
 
 all: ansi-c$(LIBEXT)
 
@@ -119,6 +120,8 @@ cprover_library.cpp: cprover_library.inc
 ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_generic.inc
 ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_ia32.inc
 ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_ia32-2.inc
+ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_ia32-3.inc
+ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_ia32-4.inc
 ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_alpha.inc
 ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_arm.inc
 ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_math.inc
@@ -140,7 +143,8 @@ generated_files: cprover_library.inc gcc_builtin_headers_generic.inc \
 	ansi_c_y.tab.h clang_builtin_headers.inc gcc_builtin_headers_ia32-2.inc \
   gcc_builtin_headers_math.inc gcc_builtin_headers_omp.inc \
   gcc_builtin_headers_tm.inc gcc_builtin_headers_ubsan.inc \
-  gcc_builtin_headers_mem_string.inc
+  gcc_builtin_headers_mem_string.inc \
+  gcc_builtin_headers_ia32-3.inc gcc_builtin_headers_ia32-4.inc
 
 ###############################################################################
 

src/ansi-c/ansi_c_internal_additions.cpp

@@ -47,6 +47,12 @@ const char gcc_builtin_headers_ia32[]=
 const char gcc_builtin_headers_ia32_2[]=
 #include "gcc_builtin_headers_ia32-2.inc"
 ; // NOLINT(whitespace/semicolon)
+const char gcc_builtin_headers_ia32_3[]=
+#include "gcc_builtin_headers_ia32-3.inc"
+; // NOLINT(whitespace/semicolon)
+const char gcc_builtin_headers_ia32_4[]=
+#include "gcc_builtin_headers_ia32-4.inc"
+; // NOLINT(whitespace/semicolon)
 
 const char gcc_builtin_headers_alpha[]=
 "# 1 \"gcc_builtin_headers_alpha.h\"\n"
@@ -286,6 +292,8 @@ void ansi_c_internal_additions(std::string &code)
 
       code+=gcc_builtin_headers_ia32;
       code+=gcc_builtin_headers_ia32_2;
+      code+=gcc_builtin_headers_ia32_3;
+      code+=gcc_builtin_headers_ia32_4;
     }
     else if(config.ansi_c.arch=="arm64" ||
             config.ansi_c.arch=="armel" ||

src/ansi-c/ansi_c_internal_additions.h

@@ -22,6 +22,9 @@ extern const char gcc_builtin_headers_tm[];
 extern const char gcc_builtin_headers_ubsan[];
 extern const char clang_builtin_headers[];
 extern const char gcc_builtin_headers_ia32[];
+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 arm_builtin_headers[];
 
 #endif // CPROVER_ANSI_C_ANSI_C_INTERNAL_ADDITIONS_H

src/ansi-c/gcc_builtin_headers_ia32-3.h

@@ -256,9 +256,9 @@ while read line ; do
   if [[ $bi =~ __builtin_ia32 ]] ; then
     if grep -wq $bi gcc_builtin_headers_ia32*.h ; then
       if [ $sed_is_gnu_sed -eq 1 ] ; then
-        sed -i "/[^/].*$bi(/ s/.*/$line/" gcc_builtin_headers_ia32*.h
+        sed -i "/^[^/].*$bi(/ s/.*/$line/" gcc_builtin_headers_ia32*.h
       else
-        sed -i '' "/[^/].*$bi(/ s/.*/$line/" gcc_builtin_headers_ia32*.h
+        sed -i '' "/^[^/].*$bi(/ s/.*/$line/" gcc_builtin_headers_ia32*.h
       fi
       continue
     fi

src/ansi-c/gcc_builtin_headers_ia32-4.h

@@ -147,6 +147,9 @@ void cpp_internal_additions(std::ostream &out)
        out << "typedef double __float128;\n"; // clang doesn't do __float128
 
     out << c2cpp(gcc_builtin_headers_ia32);
+    out << c2cpp(gcc_builtin_headers_ia32_2);
+    out << c2cpp(gcc_builtin_headers_ia32_3);
+    out << c2cpp(gcc_builtin_headers_ia32_4);
     out << "}" << '\n';
   }