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 #include -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 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 +#include #include #include #include @@ -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,