Updated dump-C to use the new class

Author: thk123

src/goto-instrument/dump_c.cpp

@@ -163,7 +163,8 @@ void dump_ct::operator()(std::ostream &os)
     }
 
     // we don't want to dump in full all definitions
-    if(!tag_added && ignore(symbol))
+    if(!tag_added &&
+      system_symbols.is_symbol_internal_symbol(symbol, system_headers))
       continue;
 
     if(!symbols_sorted.insert(name_str).second)
@@ -344,7 +345,7 @@ void dump_ct::convert_compound(
       ns.lookup(to_symbol_type(type).get_identifier());
     assert(symbol.is_type);
 
-    if(!ignore(symbol))
+    if(!system_symbols.is_symbol_internal_symbol(symbol, system_headers))
       convert_compound(symbol.type, unresolved, recursive, os);
   }
   else if(type.id()==ID_c_enum_tag)
@@ -353,7 +354,7 @@ void dump_ct::convert_compound(
       ns.lookup(to_c_enum_tag_type(type).get_identifier());
     assert(symbol.is_type);
 
-    if(!ignore(symbol))
+    if(!system_symbols.is_symbol_internal_symbol(symbol, system_headers))
       convert_compound(symbol.type, unresolved, recursive, os);
   }
   else if(type.id()==ID_array || type.id()==ID_pointer)
@@ -610,259 +611,6 @@ void dump_ct::convert_compound_enum(
 
 /*******************************************************************\
 
-Function: dump_ct::init_system_library_map
-
-Inputs:
-
-Outputs:
-
-Purpose:
-
-\*******************************************************************/
-
-#define ADD_TO_SYSTEM_LIBRARY(v, header) \
-  for(size_t i=0; i<sizeof(v)/sizeof(char*); ++i) \
-    system_library_map.insert( \
-      std::make_pair(v[i], header))
-
-void dump_ct::init_system_library_map()
-{
-  // ctype.h
-  const char* ctype_syms[]=
-  {
-    "isalnum", "isalpha", "isblank", "iscntrl", "isdigit", "isgraph",
-    "islower", "isprint", "ispunct", "isspace", "isupper", "isxdigit",
-    "tolower", "toupper"
-  };
-  ADD_TO_SYSTEM_LIBRARY(ctype_syms, "ctype.h");
-
-  // fcntl.h
-  const char* fcntl_syms[]=
-  {
-    "creat", "fcntl", "open"
-  };
-  ADD_TO_SYSTEM_LIBRARY(fcntl_syms, "fcntl.h");
-
-  // locale.h
-  const char* locale_syms[]=
-  {
-    "setlocale"
-  };
-  ADD_TO_SYSTEM_LIBRARY(locale_syms, "locale.h");
-
-  // math.h
-  const char* math_syms[]=
-  {
-    "acos", "acosh", "asin", "asinh", "atan", "atan2", "atanh",
-    "cbrt", "ceil", "copysign", "cos", "cosh", "erf", "erfc", "exp",
-    "exp2", "expm1", "fabs", "fdim", "floor", "fma", "fmax", "fmin",
-    "fmod", "fpclassify", "frexp", "hypot", "ilogb", "isfinite",
-    "isinf", "isnan", "isnormal", "j0", "j1", "jn", "ldexp", "lgamma",
-    "llrint", "llround", "log", "log10", "log1p", "log2", "logb",
-    "lrint", "lround", "modf", "nan", "nearbyint", "nextafter", "pow",
-    "remainder", "remquo", "rint", "round", "scalbln", "scalbn",
-    "signbit", "sin", "sinh", "sqrt", "tan", "tanh", "tgamma",
-    "trunc", "y0", "y1", "yn"
-  };
-  ADD_TO_SYSTEM_LIBRARY(math_syms, "math.h");
-
-  // pthread.h
-  const char* pthread_syms[]=
-  {
-    "pthread_cleanup_pop", "pthread_cleanup_push",
-    "pthread_cond_broadcast", "pthread_cond_destroy",
-    "pthread_cond_init", "pthread_cond_signal",
-    "pthread_cond_timedwait", "pthread_cond_wait", "pthread_create",
-    "pthread_detach", "pthread_equal", "pthread_exit",
-    "pthread_getspecific", "pthread_join", "pthread_key_delete",
-    "pthread_mutex_destroy", "pthread_mutex_init",
-    "pthread_mutex_lock", "pthread_mutex_trylock",
-    "pthread_mutex_unlock", "pthread_once", "pthread_rwlock_destroy",
-    "pthread_rwlock_init", "pthread_rwlock_rdlock",
-    "pthread_rwlock_unlock", "pthread_rwlock_wrlock",
-    "pthread_rwlockattr_destroy", "pthread_rwlockattr_getpshared",
-    "pthread_rwlockattr_init", "pthread_rwlockattr_setpshared",
-    "pthread_self", "pthread_setspecific"
-  };
-  ADD_TO_SYSTEM_LIBRARY(pthread_syms, "pthread.h");
-
-  // setjmp.h
-  const char* setjmp_syms[]=
-  {
-    "_longjmp", "_setjmp", "longjmp", "longjmperror", "setjmp",
-    "siglongjmp", "sigsetjmp"
-  };
-  ADD_TO_SYSTEM_LIBRARY(setjmp_syms, "setjmp.h");
-
-  // stdio.h
-  const char* stdio_syms[]=
-  {
-    "asprintf", "clearerr", "fclose", "fdopen", "feof", "ferror",
-    "fflush", "fgetc", "fgetln", "fgetpos", "fgets", "fgetwc",
-    "fgetws", "fileno", "fopen", "fprintf", "fpurge", "fputc",
-    "fputs", "fputwc", "fputws", "fread", "freopen", "fropen",
-    "fscanf", "fseek", "fsetpos", "ftell", "funopen", "fwide",
-    "fwopen", "fwprintf", "fwrite", "getc", "getchar", "getdelim",
-    "getline", "gets", "getw", "getwc", "getwchar", "mkdtemp",
-    "mkstemp", "mktemp", "perror", "printf", "putc", "putchar",
-    "puts", "putw", "putwc", "putwchar", "remove", "rewind", "scanf",
-    "setbuf", "setbuffer", "setlinebuf", "setvbuf", "snprintf",
-    "sprintf", "sscanf", "strerror", "swprintf", "sys_errlist",
-    "sys_nerr", "tempnam", "tmpfile", "tmpnam", "ungetc", "ungetwc",
-    "vasprintf", "vfprintf", "vfscanf", "vfwprintf", "vprintf",
-    "vscanf", "vsnprintf", "vsprintf", "vsscanf", "vswprintf",
-    "vwprintf", "wprintf",
-    /* non-public struct types */
-    "tag-__sFILE", "tag-__sbuf", // OS X
-    "tag-_IO_FILE", "tag-_IO_marker", // Linux
-  };
-  ADD_TO_SYSTEM_LIBRARY(stdio_syms, "stdio.h");
-
-  // stdlib.h
-  const char* stdlib_syms[]=
-  {
-    "abort", "abs", "atexit", "atof", "atoi", "atol", "atoll",
-    "bsearch", "calloc", "div", "exit", "free", "getenv", "labs",
-    "ldiv", "llabs", "lldiv", "malloc", "mblen", "mbstowcs", "mbtowc",
-    "qsort", "rand", "realloc", "srand", "strtod", "strtof", "strtol",
-    "strtold", "strtoll", "strtoul", "strtoull", "system", "wcstombs",
-    "wctomb"
-  };
-  ADD_TO_SYSTEM_LIBRARY(stdlib_syms, "stdlib.h");
-
-  // string.h
-  const char* string_syms[]=
-  {
-    "strcat", "strncat", "strchr", "strrchr", "strcmp", "strncmp",
-    "strcpy", "strncpy", "strerror", "strlen", "strpbrk", "strspn",
-    "strcspn", "strstr", "strtok"
-  };
-  ADD_TO_SYSTEM_LIBRARY(string_syms, "string.h");
-
-  // time.h
-  const char* time_syms[]=
-  {
-    "asctime", "asctime_r", "ctime", "ctime_r", "difftime", "gmtime",
-    "gmtime_r", "localtime", "localtime_r", "mktime",
-    /* non-public struct types */
-    "tag-timespec", "tag-timeval"
-  };
-  ADD_TO_SYSTEM_LIBRARY(time_syms, "time.h");
-
-  // unistd.h
-  const char* unistd_syms[]=
-  {
-    "_exit", "access", "alarm", "chdir", "chown", "close", "dup",
-    "dup2", "execl", "execle", "execlp", "execv", "execve", "execvp",
-    "fork", "fpathconf", "getcwd", "getegid", "geteuid", "getgid",
-    "getgroups", "getlogin", "getpgrp", "getpid", "getppid", "getuid",
-    "isatty", "link", "lseek", "pathconf", "pause", "pipe", "read",
-    "rmdir", "setgid", "setpgid", "setsid", "setuid", "sleep",
-    "sysconf", "tcgetpgrp", "tcsetpgrp", "ttyname", "ttyname_r",
-    "unlink", "write"
-  };
-  ADD_TO_SYSTEM_LIBRARY(unistd_syms, "unistd.h");
-
-  // sys/select.h
-  const char* sys_select_syms[]=
-  {
-    "select"
-  };
-  ADD_TO_SYSTEM_LIBRARY(sys_select_syms, "sys/select.h");
-
-  // sys/socket.h
-  const char* sys_socket_syms[]=
-  {
-    "accept", "bind", "connect"
-  };
-  ADD_TO_SYSTEM_LIBRARY(sys_socket_syms, "sys/socket.h");
-
-  // sys/stat.h
-  const char* sys_stat_syms[]=
-  {
-    "fstat", "lstat", "stat"
-  };
-  ADD_TO_SYSTEM_LIBRARY(sys_stat_syms, "sys/stat.h");
-
-  /*
-  // sys/types.h
-  const char* sys_types_syms[]=
-  {
-  };
-  ADD_TO_SYSTEM_LIBRARY(sys_types_syms, "sys/types.h");
-  */
-
-  // sys/wait.h
-  const char* sys_wait_syms[]=
-  {
-    "wait", "waitpid"
-  };
-  ADD_TO_SYSTEM_LIBRARY(sys_wait_syms, "sys/wait.h");
-}
-
-/*******************************************************************\
-
-Function: dump_ct::ignore
-
-Inputs:
-
-Outputs:
-
-Purpose:
-
-\*******************************************************************/
-
-bool dump_ct::ignore(const symbolt &symbol)
-{
-  const std::string &name_str=id2string(symbol.name);
-
-  if(has_prefix(name_str, CPROVER_PREFIX) ||
-     name_str=="__func__" ||
-     name_str=="__FUNCTION__" ||
-     name_str=="__PRETTY_FUNCTION__" ||
-     name_str=="argc'" ||
-     name_str=="argv'" ||
-     name_str=="envp'" ||
-     name_str=="envp_size'")
-    return true;
-
-  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") &&
-     has_prefix(name_str, "__builtin_"))
-    return true;
-
-  if(name_str=="__builtin_va_start" ||
-     name_str=="__builtin_va_end" ||
-     symbol.name==ID_gcc_builtin_va_arg)
-  {
-    system_headers.insert("stdarg.h");
-    return true;
-  }
-
-  if(name_str.find("$link")!=std::string::npos)
-    return false;
-
-  system_library_mapt::const_iterator it=
-    system_library_map.find(symbol.name);
-
-  if(it!=system_library_map.end())
-  {
-    system_headers.insert(it->second);
-    return true;
-  }
-
-  return false;
-}
-
-/*******************************************************************\
-
 Function: dump_ct::cleanup_decl
 
 Inputs:

src/goto-instrument/dump_c_class.h

@@ -15,6 +15,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/language.h>
 
 #include <langapi/mode.h>
+#include <goto-programs/system_library_symbols.h>
 
 class dump_ct
 {
@@ -30,7 +31,7 @@ class dump_ct
     language(factory())
   {
     if(use_system_headers)
-      init_system_library_map();
+      system_symbols=system_library_symbolst();
   }
 
   virtual ~dump_ct()
@@ -51,21 +52,15 @@ class dump_ct
 
   std::set<std::string> system_headers;
 
-  typedef std::unordered_map<irep_idt, std::string, irep_id_hash>
-    system_library_mapt;
-  system_library_mapt system_library_map;
+  system_library_symbolst system_symbols;
 
   typedef std::unordered_map<irep_idt, irep_idt, irep_id_hash>
     declared_enum_constants_mapt;
   declared_enum_constants_mapt declared_enum_constants;
 
-  void init_system_library_map();
-
   std::string type_to_string(const typet &type);
   std::string expr_to_string(const exprt &expr);
 
-  bool ignore(const symbolt &symbol);
-
   static std::string indent(const unsigned n)
   {
     return std::string(2*n, ' ');

src/goto-programs/system_library_symbols.cpp

@@ -284,7 +284,7 @@ Purpose: To find out if a symbol is an internal symbol.
 
 bool system_library_symbolst::is_symbol_internal_symbol(
   const symbolt &symbol,
-  std::set<irep_idt> &out_system_headers) const
+  std::set<std::string> &out_system_headers) const
 {
   const std::string &name_str=id2string(symbol.name);
 
@@ -345,7 +345,7 @@ bool system_library_symbolst::is_symbol_internal_symbol(
 
   if(it!=system_library_map.end())
   {
-    out_system_headers.insert(it->second);
+    out_system_headers.insert(id2string(it->second));
     return true;
   }
 

src/goto-programs/system_library_symbols.h

@@ -11,6 +11,7 @@ Author: Thomas Kiley
 
 #include <list>
 #include <set>
+#include <string>
 #include <util/irep.h>
 
 class symbolt;
@@ -22,7 +23,7 @@ class system_library_symbolst
 
   bool is_symbol_internal_symbol(
     const symbolt &symbol,
-    std::set<irep_idt> &out_system_headers) const;
+    std::set<std::string> &out_system_headers) const;
 
 private:
   void init_system_library_map();