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 @@ -829,12 +829,7 @@ bool dump_ct::ignore(const symbolt &symbol)
829
829
const std::string &file_str=id2string (symbol.location .get_file ());
830
830
831
831
// don't dump internal GCC builtins
832
- if ((file_str==" gcc_builtin_headers_alpha.h" ||
833
- file_str==" gcc_builtin_headers_arm.h" ||
834
- file_str==" gcc_builtin_headers_ia32.h" ||
835
- file_str==" gcc_builtin_headers_mips.h" ||
836
- file_str==" gcc_builtin_headers_power.h" ||
837
- file_str==" gcc_builtin_headers_generic.h" ) &&
832
+ if (has_prefix (file_str, " gcc_builtin_headers_" ) &&
838
833
has_prefix (name_str, " __builtin_" ))
839
834
return true ;
840
835
@@ -857,6 +852,14 @@ bool dump_ct::ignore(const symbolt &symbol)
857
852
system_headers.insert (it->second );
858
853
return true ;
859
854
}
855
+ else if (!system_library_map.empty () &&
856
+ has_prefix (file_str, " /usr/include/" ) &&
857
+ file_str.find (" /bits/" )==std::string::npos)
858
+ {
859
+ system_headers.insert (
860
+ file_str.substr (std::string (" /usr/include/" ).size ()));
861
+ return true ;
862
+ }
860
863
861
864
return false ;
862
865
}
You can’t perform that action at this time.
0 commit comments