Skip to content

Commit ebde8aa

Browse files
committed
export-file-local-symbols: handling files with many functions
The use of --export-file-local-symbols entails renaming of file-local (function) symbols with a prefix of __CPROVER_file_local, which had the side effect of those names being added as defines when building hybrid binaries. For files with large numbers of static functions, this resulted in a command-line that exceeds operating-system limits.
1 parent dac6c0c commit ebde8aa

File tree

1 file changed

+3
-0
lines changed

1 file changed

+3
-0
lines changed

src/goto-cc/compile.cpp

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -748,6 +748,9 @@ bool compilet::add_written_cprover_symbols(const symbol_tablet &symbol_table)
748748
if(!(has_prefix(id2string(name), CPROVER_PREFIX) && new_type.id()==ID_code))
749749
continue;
750750

751+
if(has_prefix(id2string(name), FILE_LOCAL_PREFIX))
752+
continue;
753+
751754
bool inserted;
752755
std::map<irep_idt, symbolt>::iterator old;
753756
std::tie(old, inserted)=written_macros.insert({name, pair.second});

0 commit comments

Comments
 (0)