dump-c: Try to guess further system headers

Author: tautschnig

CHANGELOG

@@ -8,6 +8,7 @@
 * GOTO-ANALYZER: New option --unreachable-functions, --reachable-functions
 * GOTO-INSTRUMENT: New option --undefined-function-is-assume-false
 * GOTO-INSTRUMENT: New option --remove-function-body
+* GOTO-INSTRUMENT: New option --use-all-headers
 
 
 5.7

src/clobber/clobber_parse_options.cpp

@@ -146,7 +146,7 @@ int clobber_parse_optionst::doit()
     if(!out)
       throw std::string("failed to create file simulator.c");
 
-    dump_c(goto_functions, true, ns, out);
+    dump_c(goto_functions, true, false, ns, out);
 
     status() << "instrumentation complete; compile and execute simulator.c"
              << eom;

src/goto-instrument/dump_c.cpp

@@ -732,12 +732,7 @@ bool dump_ct::ignore(const symbolt &symbol)
   const std::string &file_str=id2string(symbol.location.get_file());
 
   // don't dump internal GCC builtins
-  if((file_str=="gcc_builtin_headers_alpha.h" ||
-      file_str=="gcc_builtin_headers_arm.h" ||
-      file_str=="gcc_builtin_headers_ia32.h" ||
-      file_str=="gcc_builtin_headers_mips.h" ||
-      file_str=="gcc_builtin_headers_power.h" ||
-      file_str=="gcc_builtin_headers_generic.h") &&
+  if(has_prefix(file_str, "gcc_builtin_headers_") &&
      has_prefix(name_str, "__builtin_"))
     return true;
 
@@ -761,6 +756,19 @@ bool dump_ct::ignore(const symbolt &symbol)
     return true;
   }
 
+  if(use_all_headers &&
+     has_prefix(file_str, "/usr/include/"))
+  {
+    if(file_str.find("/bits/")==std::string::npos)
+    {
+      // Do not include transitive includes of system headers!
+      std::string::size_type prefix_len=std::string("/usr/include/").size();
+      system_headers.insert(file_str.substr(prefix_len));
+    }
+
+    return true;
+  }
+
   return false;
 }
 
@@ -1278,19 +1286,23 @@ std::string dump_ct::expr_to_string(const exprt &expr)
 void dump_c(
   const goto_functionst &src,
   const bool use_system_headers,
+  const bool use_all_headers,
   const namespacet &ns,
   std::ostream &out)
 {
-  dump_ct goto2c(src, use_system_headers, ns, new_ansi_c_language);
+  dump_ct goto2c(
+    src, use_system_headers, use_all_headers, ns, new_ansi_c_language);
   out << goto2c;
 }
 
 void dump_cpp(
   const goto_functionst &src,
   const bool use_system_headers,
+  const bool use_all_headers,
   const namespacet &ns,
   std::ostream &out)
 {
-  dump_ct goto2cpp(src, use_system_headers, ns, new_cpp_language);
+  dump_ct goto2cpp(
+    src, use_system_headers, use_all_headers, ns, new_cpp_language);
   out << goto2cpp;
 }

src/goto-instrument/dump_c.h

@@ -17,12 +17,14 @@ Author: Daniel Kroening, [email protected]
 void dump_c(
   const goto_functionst &src,
   const bool use_system_headers,
+  const bool use_all_headers,
   const namespacet &ns,
   std::ostream &out);
 
 void dump_cpp(
   const goto_functionst &src,
   const bool use_system_headers,
+  const bool use_all_headers,
   const namespacet &ns,
   std::ostream &out);
 

src/goto-instrument/dump_c_class.h

@@ -25,12 +25,14 @@ class dump_ct
   dump_ct(
     const goto_functionst &_goto_functions,
     const bool use_system_headers,
+    const bool use_all_headers,
     const namespacet &_ns,
     language_factoryt factory):
     goto_functions(_goto_functions),
     copied_symbol_table(_ns.get_symbol_table()),
     ns(copied_symbol_table),
-    language(factory())
+    language(factory()),
+    use_all_headers(use_all_headers)
   {
     if(use_system_headers)
       init_system_library_map();
@@ -48,6 +50,7 @@ class dump_ct
   symbol_tablet copied_symbol_table;
   const namespacet ns;
   languaget *language;
+  const bool use_all_headers;
 
   typedef std::unordered_set<irep_idt, irep_id_hash> convertedt;
   convertedt converted_compound, converted_global, converted_enum;

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -608,7 +608,8 @@ int goto_instrument_parse_optionst::doit()
     if(cmdline.isset("dump-c") || cmdline.isset("dump-cpp"))
     {
       const bool is_cpp=cmdline.isset("dump-cpp");
-      const bool h=cmdline.isset("use-system-headers");
+      const bool h_libc=cmdline.isset("use-system-headers");
+      const bool h_all=cmdline.isset("use-all-headers");
       namespacet ns(symbol_table);
 
       // restore RETURN instructions in case remove_returns had been
@@ -627,10 +628,11 @@ int goto_instrument_parse_optionst::doit()
           error() << "failed to write to `" << cmdline.args[1] << "'";
           return 10;
         }
-        (is_cpp ? dump_cpp : dump_c)(goto_functions, h, ns, out);
+        (is_cpp ? dump_cpp : dump_c)(goto_functions, h_libc, h_all, ns, out);
       }
       else
-        (is_cpp ? dump_cpp : dump_c)(goto_functions, h, ns, std::cout);
+        (is_cpp ? dump_cpp : dump_c)(
+          goto_functions, h_libc, h_all, ns, std::cout);
 
       return 0;
     }
@@ -1482,7 +1484,7 @@ void goto_instrument_parse_optionst::help()
     " --check-invariant function   instruments invariant checking function\n"
     " --remove-pointers            converts pointer arithmetic to base+offset expressions\n" // NOLINT(*)
     " --undefined-function-is-assume-false\n"
-    "                              convert each call to an undefined function to assume(false)\n"
+    "                              convert each call to an undefined function to assume(false)\n" // NOLINT(*)
     "\n"
     "Loop transformations:\n"
     " --k-induction <k>            check loops with k-induction\n"
@@ -1526,7 +1528,8 @@ void goto_instrument_parse_optionst::help()
     " --remove-function-body <f>   remove the implementation of function <f> (may be repeated)\n"
     "\n"
     "Other options:\n"
-    " --use-system-headers         with --dump-c/--dump-cpp: generate C source with includes\n" // NOLINT(*)
+    " --use-system-headers         with --dump-c/--dump-cpp: generate C source with libc includes\n" // NOLINT(*)
+    " --use-all-headers            with --dump-c/--dump-cpp: generate C source with all includes\n" // NOLINT(*)
     " --version                    show version and exit\n"
     " --xml-ui                     use XML-formatted output\n"
     " --json-ui                    use JSON-formatted output\n"

src/goto-instrument/goto_instrument_parse_options.h

@@ -26,7 +26,7 @@ Author: Daniel Kroening, [email protected]
   "(all)" \
   "(document-claims-latex)(document-claims-html)" \
   "(document-properties-latex)(document-properties-html)" \
-  "(dump-c)(dump-cpp)(use-system-headers)(dot)(xml)" \
+  "(dump-c)(dump-cpp)(use-system-headers)(use-all-headers)(dot)(xml)" \
   OPT_GOTO_CHECK \
   /* no-X-check are deprecated and ignored */ \
   "(no-bounds-check)(no-pointer-check)(no-div-by-zero-check)" \