From d7121f268646165a67b3fde26a54415731ee4491 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Mon, 7 Aug 2017 09:29:38 +0000
Subject: [PATCH] dump-c: fix support of use-system-headers

As two code branches developed independently, the support for
"use-system-headers" was not fully incorporated in b7d828bc18. This commit
re-adds this support for dump-c.

Also fixes the known system headers, which include errno.h, but not errno.c and
neither noop.c.
---
 src/goto-instrument/dump_c_class.h           |  5 ++---
 src/goto-programs/system_library_symbols.cpp | 13 ++++---------
 src/goto-programs/system_library_symbols.h   |  8 +++++++-
 3 files changed, 13 insertions(+), 13 deletions(-)

diff --git a/src/goto-instrument/dump_c_class.h b/src/goto-instrument/dump_c_class.h
index bddb1cdeda2..904861fa5bd 100644
--- a/src/goto-instrument/dump_c_class.h
+++ b/src/goto-instrument/dump_c_class.h
@@ -35,10 +35,9 @@ class dump_ct
     copied_symbol_table(_ns.get_symbol_table()),
     ns(copied_symbol_table),
     language(factory()),
-    harness(include_harness)
+    harness(include_harness),
+    system_symbols(use_system_headers)
   {
-    if(use_system_headers)
-      system_symbols=system_library_symbolst();
     system_symbols.set_use_all_headers(use_all_headers);
   }
 
diff --git a/src/goto-programs/system_library_symbols.cpp b/src/goto-programs/system_library_symbols.cpp
index d6ee5ee1d34..63608caa57b 100644
--- a/src/goto-programs/system_library_symbols.cpp
+++ b/src/goto-programs/system_library_symbols.cpp
@@ -17,10 +17,11 @@ Author: Thomas Kiley
 #include <util/type.h>
 #include <sstream>
 
-system_library_symbolst::system_library_symbolst():
+system_library_symbolst::system_library_symbolst(bool init):
   use_all_headers(false)
 {
-  init_system_library_map();
+  if(init)
+    init_system_library_map();
 }
 
 /// To generate a map of header file names -> list of symbols The symbol names
@@ -220,13 +221,7 @@ void system_library_symbolst::init_system_library_map()
   {
     "__error", "__errno_location", "__errno"
   };
-  add_to_system_library("errno.c", errno_syms);
-
-  std::list<irep_idt> noop_syms=
-  {
-    "__noop"
-  };
-  add_to_system_library("noop.c", noop_syms);
+  add_to_system_library("errno.h", errno_syms);
 
 #if 0
   // sys/types.h
diff --git a/src/goto-programs/system_library_symbols.h b/src/goto-programs/system_library_symbols.h
index 82146991be1..6239508817f 100644
--- a/src/goto-programs/system_library_symbols.h
+++ b/src/goto-programs/system_library_symbols.h
@@ -13,6 +13,7 @@ Author: Thomas Kiley
 #define CPROVER_GOTO_PROGRAMS_SYSTEM_LIBRARY_SYMBOLS_H
 
 #include <list>
+#include <map>
 #include <set>
 #include <string>
 #include <util/irep.h>
@@ -24,7 +25,12 @@ class typet;
 class system_library_symbolst
 {
 public:
-  system_library_symbolst();
+  explicit system_library_symbolst(bool init);
+
+  system_library_symbolst():
+    system_library_symbolst(true) // NOLINT(runtime/explicit)
+  {
+  }
 
   bool is_symbol_internal_symbol(
     const symbolt &symbol,