Skip to content

Commit c05a91f

Browse files
author
Daniel Kroening
committed
cleanout
1 parent c58c6db commit c05a91f

File tree

3 files changed

+8
-79
lines changed

3 files changed

+8
-79
lines changed

src/goto-cc/goto_cc_main.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -107,7 +107,7 @@ int main(int argc, const char **argv)
107107
{
108108
// this simulates "ld" for linking
109109
ld_cmdlinet cmdline;
110-
ld_modet ld_mode(cmdline, base_name, true);
110+
ld_modet ld_mode(cmdline, base_name);
111111
return ld_mode.main(argc, argv);
112112
}
113113
else if(base_name.find("goto-bcc")!=std::string::npos)

src/goto-cc/ld_mode.cpp

+6-74
Original file line numberDiff line numberDiff line change
@@ -102,10 +102,8 @@ static std::string linker_name(
102102

103103
ld_modet::ld_modet(
104104
goto_cc_cmdlinet &_cmdline,
105-
const std::string &_base_name,
106-
bool _produce_hybrid_binary):
105+
const std::string &_base_name):
107106
goto_cc_modet(_cmdline, _base_name, gcc_message_handler),
108-
produce_hybrid_binary(_produce_hybrid_binary),
109107
goto_binary_tmp_suffix(".goto-cc-saved"),
110108

111109
// Keys are architectures specified in configt::set_arch().
@@ -302,8 +300,7 @@ ld_modet::ld_modet(
302300
/// does it.
303301
int ld_modet::doit()
304302
{
305-
if(cmdline.isset('?') ||
306-
cmdline.isset("help"))
303+
if(cmdline.isset("help"))
307304
{
308305
help();
309306
return EX_OK;
@@ -313,95 +310,33 @@ int ld_modet::doit()
313310

314311
auto default_verbosity = (cmdline.isset("Wall") || cmdline.isset("Wextra")) ?
315312
messaget::M_WARNING : messaget::M_ERROR;
313+
316314
eval_verbosity(
317315
cmdline.get_value("verbosity"), default_verbosity, gcc_message_handler);
318316

319-
if((cmdline.isset('v') && cmdline.have_infile_arg()) ||
320-
(cmdline.isset("version") && !produce_hybrid_binary))
321-
{
322-
// "-v" a) prints the version and b) increases verbosity.
323-
// Compilation continues, don't exit!
324-
325-
std::cout << "GNU ld version 2.16.91 20050610 (goto-cc " CBMC_VERSION
326-
<< ")\n";
327-
}
328-
329317
compilet compiler(cmdline,
330318
gcc_message_handler,
331319
cmdline.isset("Werror") &&
332320
cmdline.isset("Wextra") &&
333321
!cmdline.isset("Wno-error"));
334322

335323
if(cmdline.isset("version"))
336-
{
337-
if(produce_hybrid_binary)
338-
return run_ld(compiler);
339-
340-
std::cout << '\n' <<
341-
"Copyright (C) 2006-2014 Daniel Kroening, Christoph Wintersteiger\n" <<
342-
"CBMC version: " CBMC_VERSION << '\n' <<
343-
"Architecture: " << config.this_architecture() << '\n' <<
344-
"OS: " << config.this_operating_system() << '\n';
345-
346-
return EX_OK; // Exit!
347-
}
324+
return run_ld(compiler);
348325

349326
if(
350327
cmdline.isset("dumpmachine") || cmdline.isset("dumpspecs") ||
351328
cmdline.isset("dumpversion") || cmdline.isset("print-sysroot") ||
352329
cmdline.isset("print-sysroot-headers-suffix"))
353330
{
354-
if(produce_hybrid_binary)
355-
return run_ld(compiler);
356-
357-
// GCC will only print one of these, even when multiple arguments are
358-
// passed, so we do the same
359-
if(cmdline.isset("dumpmachine"))
360-
std::cout << config.this_architecture() << '\n';
361-
else if(cmdline.isset("dumpversion"))
362-
std::cout << "3.4.4\n";
363-
364-
// we don't have any meaningful output for the other options, and GCC
365-
// doesn't necessarily produce non-empty output either
366-
367-
return EX_OK;
331+
return run_ld(compiler);
368332
}
369333

370-
if(produce_hybrid_binary)
371-
debug() << "LD mode (hybrid)" << eom;
372-
else
373-
debug() << "LD mode" << eom;
374-
375334
// determine actions to be undertaken
376335
compiler.mode=compilet::LINK_LIBRARY;
377336

378337
// get configuration
379338
config.set(cmdline);
380339

381-
// Intel-specific
382-
// in GCC, m16 is 32-bit (!), as documented here:
383-
// https://gcc.gnu.org/bugzilla/show_bug.cgi?id=59672
384-
if(cmdline.isset("m16") ||
385-
cmdline.isset("m32") || cmdline.isset("mx32"))
386-
{
387-
config.ansi_c.arch="i386";
388-
config.ansi_c.set_arch_spec_i386();
389-
}
390-
else if(cmdline.isset("m64"))
391-
{
392-
config.ansi_c.arch="x86_64";
393-
config.ansi_c.set_arch_spec_x86_64();
394-
}
395-
396-
// ARM-specific
397-
if(cmdline.isset("mbig-endian") || cmdline.isset("mbig"))
398-
config.ansi_c.endianness=configt::ansi_ct::endiannesst::IS_BIG_ENDIAN;
399-
else if(cmdline.isset("little-endian") || cmdline.isset("mlittle"))
400-
config.ansi_c.endianness=configt::ansi_ct::endiannesst::IS_LITTLE_ENDIAN;
401-
402-
if(cmdline.isset("mthumb") || cmdline.isset("mthumb-interwork"))
403-
config.ansi_c.set_arch_spec_arm("armhf");
404-
405340
// -mcpu sets both the arch and tune, but should only be used if
406341
// neither -march nor -mtune are passed on the command line.
407342
std::string target_cpu=
@@ -488,10 +423,7 @@ int ld_modet::doit()
488423

489424
// We can generate hybrid ELF and Mach-O binaries
490425
// containing both executable machine code and the goto-binary.
491-
if(produce_hybrid_binary)
492-
return gcc_hybrid_binary(compiler);
493-
494-
return EX_OK;
426+
return gcc_hybrid_binary(compiler);
495427
}
496428

497429
int ld_modet::run_ld(const compilet &compiler)

src/goto-cc/ld_mode.h

+1-4
Original file line numberDiff line numberDiff line change
@@ -29,14 +29,11 @@ class ld_modet:public goto_cc_modet
2929

3030
ld_modet(
3131
goto_cc_cmdlinet &_cmdline,
32-
const std::string &_base_name,
33-
bool _produce_hybrid_binary);
32+
const std::string &_base_name);
3433

3534
protected:
3635
gcc_message_handlert gcc_message_handler;
3736

38-
const bool produce_hybrid_binary;
39-
4037
std::string native_tool_name;
4138

4239
const std::string goto_binary_tmp_suffix;

0 commit comments

Comments
 (0)