@@ -38,12 +38,25 @@ int linker_script_merget::add_linker_script_definitions()
3838 const std::string &elf_file=*elf_binaries.begin ();
3939 const std::string &goto_file=*goto_binaries.begin ();
4040
41- jsont data ;
41+ temporary_filet linker_def_outfile ( " goto-cc-linker-info " , " .json " ) ;
4242 std::list<irep_idt> linker_defined_symbols;
43- int fail=get_linker_script_data (
44- data, linker_defined_symbols, compiler.symbol_table , elf_file);
43+ int fail=
44+ get_linker_script_data (
45+ linker_defined_symbols,
46+ compiler.symbol_table ,
47+ elf_file,
48+ linker_def_outfile ());
49+ // ignore linker script parsing failures until the code is tested more widely
50+ if (fail!=0 )
51+ return 0 ;
52+
53+ jsont data;
54+ fail=parse_json (linker_def_outfile (), get_message_handler (), data);
4555 if (fail!=0 )
56+ {
57+ error () << " Problem parsing linker script JSON data" << eom;
4658 return fail;
59+ }
4760
4861 fail=linker_data_is_malformed (data);
4962 if (fail!=0 )
@@ -625,23 +638,24 @@ int linker_script_merget::ls_data2instructions(
625638 #endif
626639
627640int linker_script_merget::get_linker_script_data (
628- jsont &linker_data,
629641 std::list<irep_idt> &linker_defined_symbols,
630642 const symbol_tablet &symbol_table,
631- const std::string &out_file)
643+ const std::string &out_file,
644+ const std::string &def_out_file)
632645{
633646 for (auto const &pair : symbol_table.symbols )
634- if (pair.second .is_extern && pair.second .value .is_nil ()
635- && pair.second .name !=" __CPROVER_memory" )
647+ if (pair.second .is_extern && pair.second .value .is_nil () &&
648+ pair.second .name !=" __CPROVER_memory" )
636649 linker_defined_symbols.push_back (pair.second .name );
637650
638651 std::ostringstream linker_def_str;
639- std::copy (linker_defined_symbols.begin (), linker_defined_symbols.end (),
640- std::ostream_iterator<irep_idt>(linker_def_str, " \n " ));
652+ std::copy (
653+ linker_defined_symbols.begin (),
654+ linker_defined_symbols.end (),
655+ std::ostream_iterator<irep_idt>(linker_def_str, " \n " ));
641656 debug () << " Linker-defined symbols: [" << linker_def_str.str () << " ]\n "
642657 << eom;
643658
644- temporary_filet linker_def_outfile (" goto-cc-linker-info" , " .json" );
645659 temporary_filet linker_def_infile (" goto-cc-linker-defs" , " " );
646660 std::ofstream linker_def_file (linker_def_infile ());
647661 linker_def_file << linker_def_str.str ();
@@ -653,29 +667,24 @@ int linker_script_merget::get_linker_script_data(
653667 " --script" , cmdline.get_value (' T' ),
654668 " --object" , out_file,
655669 " --sym-file" , linker_def_infile (),
656- " --out-file" , linker_def_outfile ()
670+ " --out-file" , def_out_file
657671 };
658- if (cmdline.isset (" verbosity" ))
659- {
660- unsigned verb=safe_string2unsigned (cmdline.get_value (" verbosity" ));
661- if (verb>9 )
662- argv.push_back (" --very-verbose" );
663- else if (verb>4 )
664- argv.push_back (" --verbose" );
665- }
666672
667- int rc=run (argv[0 ], argv, linker_def_infile (), linker_def_outfile ());
673+ if (get_message_handler ().get_verbosity ()>9 )
674+ argv.push_back (" --very-verbose" );
675+ else if (get_message_handler ().get_verbosity ()>4 )
676+ argv.push_back (" --verbose" );
677+
678+ debug () << " RUN:" ;
679+ for (std::size_t i=0 ; i<argv.size (); i++)
680+ debug () << " " << argv[i];
681+ debug () << eom;
682+
683+ int rc=run (argv[0 ], argv, linker_def_infile (), def_out_file);
668684 if (rc!=0 )
669- {
670- error () << " Problem parsing linker script" << eom;
671- return rc;
672- }
685+ warning () << " Problem parsing linker script" << eom;
673686
674- int fail=parse_json (linker_def_outfile (), get_message_handler (),
675- linker_data);
676- if (fail!=0 )
677- error () << " Problem parsing linker script JSON data" << eom;
678- return fail;
687+ return rc;
679688}
680689
681690int linker_script_merget::goto_and_object_mismatch (
0 commit comments