File tree 1 file changed +9
-6
lines changed
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)
851
851
const std::string &file_str=id2string (symbol.location .get_file ());
852
852
853
853
// 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_" ) &&
860
855
has_prefix (name_str, " __builtin_" ))
861
856
return true ;
862
857
@@ -879,6 +874,14 @@ bool dump_ct::ignore(const symbolt &symbol)
879
874
system_headers.insert (it->second );
880
875
return true ;
881
876
}
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
+ }
882
885
883
886
return false ;
884
887
}
You can’t perform that action at this time.
0 commit comments