Added further ia32 GCC built-ins

tautschnig · tautschnig · commit 3f2379453a19 · 2017-05-23T11:01:34.000+01:00
diff --git a/.gitignore b/.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
diff --git a/src/ansi-c/Makefile b/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
 
 ###############################################################################
 
diff --git a/src/ansi-c/ansi_c_internal_additions.cpp b/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" ||
diff --git a/src/ansi-c/ansi_c_internal_additions.h b/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
diff --git a/src/ansi-c/gcc_builtin_headers_ia32-3.h b/src/ansi-c/gcc_builtin_headers_ia32-3.h
diff --git a/src/ansi-c/gcc_builtin_headers_ia32-4.h b/src/ansi-c/gcc_builtin_headers_ia32-4.h
diff --git a/src/ansi-c/get-gcc-builtins.sh b/src/ansi-c/get-gcc-builtins.sh
@@ -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
diff --git a/src/cpp/cpp_internal_additions.cpp b/src/cpp/cpp_internal_additions.cpp
@@ -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';
   }
 

Original file line number	Diff line number	Diff line change
`@@ -147,6 +147,9 @@ void cpp_internal_additions(std::ostream &out)`
`147`	`147`	`out << "typedef double __float128;\n"; // clang doesn't do __float128`
`148`	`148`
`149`	`149`	`out << c2cpp(gcc_builtin_headers_ia32);`
	`150`	`+ out << c2cpp(gcc_builtin_headers_ia32_2);`
	`151`	`+ out << c2cpp(gcc_builtin_headers_ia32_3);`
	`152`	`+ out << c2cpp(gcc_builtin_headers_ia32_4);`
`150`	`153`	`out << "}" << '\n';`
`151`	`154`	`}`
`152`	`155`