Skip to content

Commit beb56e7

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 d932d6f commit beb56e7

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
@@ -745,6 +745,9 @@ bool compilet::add_written_cprover_symbols(const symbol_tablet &symbol_table)
745745
if(!(has_prefix(id2string(name), CPROVER_PREFIX) && new_type.id()==ID_code))
746746
continue;
747747

748+
if(has_prefix(id2string(name), FILE_LOCAL_PREFIX))
749+
continue;
750+
748751
bool inserted;
749752
std::map<irep_idt, symbolt>::iterator old;
750753
std::tie(old, inserted)=written_macros.insert({name, pair.second});

0 commit comments

Comments
 (0)