File tree Expand file tree Collapse file tree 1 file changed +9
-6
lines changed Expand file tree Collapse file tree 1 file changed +9
-6
lines changed Original file line number Diff line number Diff line change @@ -851,12 +851,7 @@ bool dump_ct::ignore(const symbolt &symbol)
851851 const std::string &file_str=id2string (symbol.location .get_file ());
852852
853853 // don't dump internal GCC builtins
854- if ((file_str==" gcc_builtin_headers_alpha.h" ||
855- file_str==" gcc_builtin_headers_arm.h" ||
856- file_str==" gcc_builtin_headers_ia32.h" ||
857- file_str==" gcc_builtin_headers_mips.h" ||
858- file_str==" gcc_builtin_headers_power.h" ||
859- file_str==" gcc_builtin_headers_generic.h" ) &&
854+ if (has_prefix (file_str, " gcc_builtin_headers_" ) &&
860855 has_prefix (name_str, " __builtin_" ))
861856 return true ;
862857
@@ -879,6 +874,14 @@ bool dump_ct::ignore(const symbolt &symbol)
879874 system_headers.insert (it->second );
880875 return true ;
881876 }
877+ else if (!system_library_map.empty () &&
878+ has_prefix (file_str, " /usr/include/" ) &&
879+ file_str.find (" /bits/" )==std::string::npos)
880+ {
881+ system_headers.insert (
882+ file_str.substr (std::string (" /usr/include/" ).size ()));
883+ return true ;
884+ }
882885
883886 return false ;
884887}
You can’t perform that action at this time.
0 commit comments