C/C++ internal additions: consistently use #line

We sometimes used # 1 instead of #line 1, which GCC accepts, but Visual
Studio might not actually do, or perhaps sometimes does. It certainly
failed when used with the code in cprover_library.cpp.

Author: tautschnig

src/ansi-c/ansi_c_internal_additions.cpp

@@ -16,42 +16,42 @@ Author: Daniel Kroening, [email protected]
 #include <goto-programs/adjust_float_expressions.h>
 
 const char gcc_builtin_headers_types[]=
-"# 1 \"gcc_builtin_headers_types.h\"\n"
+"#line 1 \"gcc_builtin_headers_types.h\"\n"
 #include "gcc_builtin_headers_types.inc"
 ; // NOLINT(whitespace/semicolon)
 
 const char gcc_builtin_headers_generic[]=
-"# 1 \"gcc_builtin_headers_generic.h\"\n"
+"#line 1 \"gcc_builtin_headers_generic.h\"\n"
 #include "gcc_builtin_headers_generic.inc"
 ; // NOLINT(whitespace/semicolon)
 
 const char gcc_builtin_headers_math[]=
-"# 1 \"gcc_builtin_headers_math.h\"\n"
+"#line 1 \"gcc_builtin_headers_math.h\"\n"
 #include "gcc_builtin_headers_math.inc"
 ; // NOLINT(whitespace/semicolon)
 
 const char gcc_builtin_headers_mem_string[]=
-"# 1 \"gcc_builtin_headers_mem_string.h\"\n"
+"#line 1 \"gcc_builtin_headers_mem_string.h\"\n"
 #include "gcc_builtin_headers_mem_string.inc"
 ; // NOLINT(whitespace/semicolon)
 
 const char gcc_builtin_headers_omp[]=
-"# 1 \"gcc_builtin_headers_omp.h\"\n"
+"#line 1 \"gcc_builtin_headers_omp.h\"\n"
 #include "gcc_builtin_headers_omp.inc"
 ; // NOLINT(whitespace/semicolon)
 
 const char gcc_builtin_headers_tm[]=
-"# 1 \"gcc_builtin_headers_tm.h\"\n"
+"#line 1 \"gcc_builtin_headers_tm.h\"\n"
 #include "gcc_builtin_headers_tm.inc"
 ; // NOLINT(whitespace/semicolon)
 
 const char gcc_builtin_headers_ubsan[]=
-"# 1 \"gcc_builtin_headers_ubsan.h\"\n"
+"#line 1 \"gcc_builtin_headers_ubsan.h\"\n"
 #include "gcc_builtin_headers_ubsan.inc"
 ; // NOLINT(whitespace/semicolon)
 
 const char gcc_builtin_headers_ia32[]=
-"# 1 \"gcc_builtin_headers_ia32.h\"\n"
+"#line 1 \"gcc_builtin_headers_ia32.h\"\n"
 #include "gcc_builtin_headers_ia32.inc"
 ; // NOLINT(whitespace/semicolon)
 const char gcc_builtin_headers_ia32_2[]=
@@ -68,47 +68,47 @@ const char gcc_builtin_headers_ia32_5[] =
   ; // NOLINT(whitespace/semicolon)
 
 const char gcc_builtin_headers_alpha[]=
-"# 1 \"gcc_builtin_headers_alpha.h\"\n"
+"#line 1 \"gcc_builtin_headers_alpha.h\"\n"
 #include "gcc_builtin_headers_alpha.inc"
 ; // NOLINT(whitespace/semicolon)
 
 const char gcc_builtin_headers_arm[]=
-"# 1 \"gcc_builtin_headers_arm.h\"\n"
+"#line 1 \"gcc_builtin_headers_arm.h\"\n"
 #include "gcc_builtin_headers_arm.inc"
 ; // NOLINT(whitespace/semicolon)
 
 const char gcc_builtin_headers_mips[]=
-"# 1 \"gcc_builtin_headers_mips.h\"\n"
+"#line 1 \"gcc_builtin_headers_mips.h\"\n"
 #include "gcc_builtin_headers_mips.inc"
 ; // NOLINT(whitespace/semicolon)
 
 const char gcc_builtin_headers_power[]=
-"# 1 \"gcc_builtin_headers_power.h\"\n"
+"#line 1 \"gcc_builtin_headers_power.h\"\n"
 #include "gcc_builtin_headers_power.inc"
 ; // NOLINT(whitespace/semicolon)
 
 const char arm_builtin_headers[]=
-"# 1 \"arm_builtin_headers.h\"\n"
+"#line 1 \"arm_builtin_headers.h\"\n"
 #include "arm_builtin_headers.inc"
 ; // NOLINT(whitespace/semicolon)
 
 const char cw_builtin_headers[]=
-"# 1 \"cw_builtin_headers.h\"\n"
+"#line 1 \"cw_builtin_headers.h\"\n"
 #include "cw_builtin_headers.inc"
 ; // NOLINT(whitespace/semicolon)
 
 const char clang_builtin_headers[]=
-"# 1 \"clang_builtin_headers.h\"\n"
+"#line 1 \"clang_builtin_headers.h\"\n"
 #include "clang_builtin_headers.inc"
 ; // NOLINT(whitespace/semicolon)
 
 const char cprover_builtin_headers[]=
-"# 1 \"cprover_builtin_headers.h\"\n"
+"#line 1 \"cprover_builtin_headers.h\"\n"
 #include "cprover_builtin_headers.inc"
 ; // NOLINT(whitespace/semicolon)
 
 const char windows_builtin_headers[]=
-"# 1 \"windows_builtin_headers.h\"\n"
+"#line 1 \"windows_builtin_headers.h\"\n"
 #include "windows_builtin_headers.inc"
 ; // NOLINT(whitespace/semicolon)
 
@@ -158,7 +158,7 @@ void ansi_c_internal_additions(std::string &code)
   // clang-format off
   // do the built-in types and variables
   code+=
-    "# 1 \"<built-in-additions>\"\n"
+    "#line 1 \"<built-in-additions>\"\n"
     "typedef __typeof__(sizeof(int)) " CPROVER_PREFIX "size_t;\n"
     "typedef "+c_type_as_string(signed_size_type().get(ID_C_c_type))+
       " " CPROVER_PREFIX "ssize_t;\n"
@@ -312,7 +312,7 @@ void ansi_c_architecture_strings(std::string &code)
   // They allow identifying the architectural settings used
   // at compile time from a goto-binary.
 
-  code+="# 1 \"<builtin-architecture-strings>\"\n";
+  code += "#line 1 \"<builtin-architecture-strings>\"\n";
 
   code+=architecture_string(config.ansi_c.int_width, "int_width");
   code+=architecture_string(config.ansi_c.int_width, "word_size"); // old

src/cpp/cpp_internal_additions.cpp

@@ -44,7 +44,7 @@ std::string c2cpp(const std::string &s)
 
 void cpp_internal_additions(std::ostream &out)
 {
-  out << "# 1 \"<built-in-additions>\"" << '\n';
+  out << "#line 1 \"<built-in-additions>\"" << '\n';
 
   // __CPROVER namespace
   out << "namespace __CPROVER { }" << '\n';