Merge pull request #6593 from tautschnig/cleanup/is_type_internal

Remove useless system_library_symbolst::is_type_internal

Author: tautschnig

regression/goto-instrument/dump-typedef/main.c

@@ -0,0 +1,27 @@
+#include <stdint.h>
+
+// NOLINTNEXTLINE(whitespace/line_length)
+#line 1 "/Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/usr/include/stdint.h"
+typedef short int16_t;
+
+// NOLINTNEXTLINE(whitespace/line_length)
+#line 1 "/Applications/Xcode_13.2.1.app/Contents/Developer/Platforms/MacOSX.platform/Developer/SDKs/MacOSX.sdk/usr/include/stdint.h"
+typedef unsigned short uint16_t;
+
+// NOLINTNEXTLINE(whitespace/line_length)
+#line 1 "C:\\Program Files (x86)\\Microsoft Visual Studio\\2017\\Community\\VC\\Tools\\MSVC\\14.10.25017\\include\\stdint.h"
+typedef int int32_t;
+
+// NOLINTNEXTLINE(whitespace/line_length)
+#line 1 "C:\\Program Files\\Microsoft Visual Studio\\2022\\Enterprise\\VC\\Tools\\MSVC\\14.30.30705\\include\\stdint.h"
+typedef unsigned int uint32_t;
+
+#line 20 "main.c"
+int main(int argc, char *argv[])
+{
+  intmax_t x;
+  int16_t y;
+  uint16_t uy;
+  int32_t z;
+  uint32_t uz;
+}

regression/goto-instrument/dump-typedef/test.desc

@@ -0,0 +1,13 @@
+CORE
+main.c
+--dump-c --use-all-headers
+#include <(stdint.h|_types/_intmax_t.h)>
+intmax_t
+^EXIT=0$
+^SIGNAL=0$
+--
+typedef
+^warning: ignoring
+--
+Dump-c with --use-all-headers should re-generate the #include and not print a
+local typedef statement for intmax_t instead.

src/goto-instrument/dump_c.cpp

@@ -733,9 +733,6 @@ void dump_ct::collect_typedefs_rec(
   bool early,
   std::unordered_set<irep_idt> &dependencies)
 {
-  if(system_symbols.is_type_internal(type, system_headers))
-    return;
-
   std::unordered_set<irep_idt> local_deps;
 
   if(type.id()==ID_code)

src/goto-programs/system_library_symbols.cpp

@@ -253,22 +253,6 @@ void system_library_symbolst::add_to_system_library(
   }
 }
 
-/// Helper function to call `is_symbol_internal_symbol` on a nameless
-/// fake symbol with the given type, to determine whether the type alone
-/// is sufficient to classify a symbol of that type as internal.
-/// \param type: the type to check
-/// \param [out] out_system_headers: specific system headers that need to be
-///   included
-/// \return True if the type is an internal type
-bool system_library_symbolst::is_type_internal(
-  const typet &type,
-  std::set<std::string> &out_system_headers) const
-{
-  symbolt symbol;
-  symbol.type=type;
-  return is_symbol_internal_symbol(symbol, out_system_headers);
-}
-
 /// To find out if a symbol is an internal symbol.
 /// \param symbol: the symbol to check
 /// \param [out] out_system_headers: specific system headers that need to be
@@ -336,17 +320,36 @@ bool system_library_symbolst::is_symbol_internal_symbol(
     return true;
   }
 
-  if(use_all_headers &&
-     has_prefix(file_str, "/usr/include/"))
+  if(use_all_headers)
   {
-    if(file_str.find("/bits/")==std::string::npos)
+    if(
+      has_prefix(file_str, "/usr/include/") ||
+      ((has_prefix(file_str, "/Library/Developer/") ||
+        has_prefix(file_str, "/Applications/Xcode")) &&
+       file_str.find("/usr/include/") != std::string::npos))
     {
-      // Do not include transitive includes of system headers!
-      std::string::size_type prefix_len=std::string("/usr/include/").size();
-      out_system_headers.insert(file_str.substr(prefix_len));
+      if(file_str.find("/bits/") == std::string::npos)
+      {
+        // Do not include transitive includes of system headers!
+        const std::string::size_type prefix_len =
+          file_str.find("/usr/include/") + std::string("/usr/include/").size();
+        out_system_headers.insert(file_str.substr(prefix_len));
+      }
+
+      return true;
     }
+    else if(
+      (has_prefix(
+         file_str, "C:\\Program Files (x86)\\Microsoft Visual Studio\\") ||
+       has_prefix(file_str, "C:\\Program Files\\Microsoft Visual Studio\\")) &&
+      file_str.find("\\include\\") != std::string::npos)
+    {
+      const std::string::size_type prefix_len =
+        file_str.find("\\include\\") + std::string("\\include\\").size();
+      out_system_headers.insert(file_str.substr(prefix_len));
 
-    return true;
+      return true;
+    }
   }
 
   return false;

src/goto-programs/system_library_symbols.h

@@ -35,10 +35,6 @@ class system_library_symbolst
     const symbolt &symbol,
     std::set<std::string> &out_system_headers) const;
 
-  bool is_type_internal(
-    const typet &type,
-    std::set<std::string> &out_system_headers) const;
-
   void set_use_all_headers(bool use)
   {
     use_all_headers=use;