44 const std::string &base_name)
46 if(cmdline.
isset(
"native-compiler"))
47 return cmdline.
get_value(
"native-compiler");
49 if(base_name==
"bcc" ||
50 base_name.find(
"goto-bcc")!=std::string::npos)
53 if(base_name==
"goto-clang")
56 std::string::size_type
pos=base_name.find(
"goto-gcc");
58 if(
pos==std::string::npos ||
59 base_name==
"goto-gcc" ||
62#if defined(__FreeBSD__) || defined(__OpenBSD__)
69 std::string result=base_name;
70 result.replace(
pos, 8,
"gcc");
77 const std::string &base_name)
79 if(cmdline.
isset(
"native-linker"))
80 return cmdline.
get_value(
"native-linker");
82 std::string::size_type
pos=base_name.find(
"goto-ld");
84 if(
pos==std::string::npos ||
85 base_name==
"goto-gcc" ||
89 std::string result=base_name;
90 result.replace(
pos, 7,
"ld");
97 const std::string &_base_name,
98 bool _produce_hybrid_binary):
121 "strongarm",
"strongarm110",
"strongarm1100",
"strongarm1110",
122 "arm2",
"arm250",
"arm3",
"arm6",
"arm60",
"arm600",
"arm610",
123 "arm620",
"fa526",
"fa626",
"fa606te",
"fa626te",
"fmp626",
124 "xscale",
"iwmmxt",
"iwmmxt2",
"xgene1"
127 "armv7",
"arm7m",
"arm7d",
"arm7dm",
"arm7di",
"arm7dmi",
128 "arm70",
"arm700",
"arm700i",
"arm710",
"arm710c",
"arm7100",
129 "arm720",
"arm7500",
"arm7500fe",
"arm7tdmi",
"arm7tdmi-s",
130 "arm710t",
"arm720t",
"arm740t",
"mpcore",
"mpcorenovfp",
131 "arm8",
"arm810",
"arm9",
"arm9e",
"arm920",
"arm920t",
132 "arm922t",
"arm946e-s",
"arm966e-s",
"arm968e-s",
"arm926ej-s",
133 "arm940t",
"arm9tdmi",
"arm10tdmi",
"arm1020t",
"arm1026ej-s",
134 "arm10e",
"arm1020e",
"arm1022e",
"arm1136j-s",
"arm1136jf-s",
135 "arm1156t2-s",
"arm1156t2f-s",
"arm1176jz-s",
"arm1176jzf-s",
136 "cortex-a5",
"cortex-a7",
"cortex-a8",
"cortex-a9",
137 "cortex-a12",
"cortex-a15",
"cortex-a53",
"cortex-r4",
138 "cortex-r4f",
"cortex-r5",
"cortex-r7",
"cortex-m7",
139 "cortex-m4",
"cortex-m3",
"cortex-m1",
"cortex-m0",
140 "cortex-m0plus",
"cortex-m1.small-multiply",
141 "cortex-m0.small-multiply",
"cortex-m0plus.small-multiply",
142 "marvell-pj4",
"ep9312",
"fa726te",
145 "cortex-a57",
"cortex-a72",
"exynos-m1"
147 {
"hppa", {
"1.0",
"1.1",
"2.0"}},
152 "powerpc",
"601",
"602",
"603",
"603e",
"604",
"604e",
"630",
156 "G4",
"7400",
"7450",
158 "401",
"403",
"405",
"405fp",
"440",
"440fp",
"464",
"464fp",
162 "e300c2",
"e300c3",
"e500mc",
"ec603e",
175 "power3",
"power4",
"power5",
"power5+",
"power6",
"power6x",
179 "e500mc64",
"e5500",
"e6500",
184 {
"powerpc64le", {
"powerpc64le",
"power8"}},
206 "loongson2e",
"loongson2f",
"loongson3a",
"mips64",
"mips64r2",
207 "mips64r3",
"mips64r5",
"mips64r6 4kc",
"5kc",
"5kf",
"20kc",
208 "octeon",
"octeon+",
"octeon2",
"octeon3",
"sb1",
"vr4100",
209 "vr4111",
"vr4120",
"vr4130",
"vr4300",
"vr5000",
"vr5400",
210 "vr5500",
"sr71000",
"xlp",
213 "mips32",
"mips32r2",
"mips32r3",
"mips32r5",
"mips32r6",
215 "4km",
"4kp",
"4ksc",
"4kec",
"4kem",
"4kep",
"4ksd",
"24kc",
216 "24kf2_1",
"24kf1_1",
"24kec",
"24kef2_1",
"24kef1_1",
"34kc",
217 "34kf2_1",
"34kf1_1",
"34kn",
"74kc",
"74kf2_1",
"74kf1_1",
218 "74kf3_2",
"1004kc",
"1004kf2_1",
"1004kf1_1",
"m4k",
"m14k",
219 "m14kc",
"m14ke",
"m14kec",
224 "mips1",
"mips2",
"r2000",
"r3000",
228 "mips3",
"mips4",
"r4000",
"r4400",
"r4600",
"r4650",
"r4700",
229 "r8000",
"rm7000",
"rm9000",
"r10000",
"r12000",
"r14000",
240 "z900",
"z990",
"g5",
"g6",
243 "z9-109",
"z9-ec",
"z10",
"z196",
"zEC12",
"z13"
251 "v7",
"v8",
"leon",
"leon3",
"leon3v7",
"cypress",
"supersparc",
252 "hypersparc",
"sparclite",
"f930",
"f934",
"sparclite86x",
256 "v9",
"ultrasparc",
"ultrasparc3",
"niagara",
"niagara2",
257 "niagara3",
"niagara4",
260 "itanium",
"itanium1",
"merced",
"itanium2",
"mckinley"
267 "i386",
"i486",
"i586",
"i686",
269 "k6",
"k6-2",
"k6-3",
"athlon" "athlon-tbird",
"athlon-4",
270 "athlon-xp",
"athlon-mp",
273 "pentium",
"pentium-mmx",
"pentiumpro" "pentium2",
"pentium3",
274 "pentium3m",
"pentium-m" "pentium4",
"pentium4m",
"prescott",
276 "winchip-c6",
"winchip2",
"c3",
"c3-2",
"geode",
280 "nocona",
"core2",
"nehalem" "westmere",
"sandybridge",
"knl",
281 "ivybridge",
"haswell",
"broadwell" "bonnell",
"silvermont",
283 "k8",
"k8-sse3",
"opteron",
"athlon64",
"athlon-fx",
284 "opteron-sse3" "athlon64-sse3",
"amdfam10",
"barcelona",
286 "bdver1",
"bdver2" "bdver3",
"bdver4",
314 auto default_verbosity = (
cmdline.isset(
"Wall") ||
cmdline.isset(
"Wextra")) ?
323 base_name.find(
"goto-bcc")!=std::string::npos;
335 std::cout <<
"bcc: version " <<
gcc_version <<
" (goto-cc "
340 std::cout <<
"clang version " <<
gcc_version <<
" (goto-cc "
360 <<
"Copyright (C) 2006-2018 Daniel Kroening, Christoph Wintersteiger\n"
362 <<
"Architecture: " <<
config.this_architecture() <<
'\n'
363 <<
"OS: " <<
config.this_operating_system() <<
'\n';
390 cmdline.isset(
"print-sysroot-headers-suffix"))
397 if(
cmdline.isset(
"dumpmachine"))
398 std::cout <<
config.this_architecture() <<
'\n';
399 else if(
cmdline.isset(
"dumpversion"))
435 else if(
cmdline.isset(
"shared") ||
461 config.ansi_c.arch=
"i386";
462 config.ansi_c.set_arch_spec_i386();
466 config.ansi_c.arch=
"x86_64";
467 config.ansi_c.set_arch_spec_x86_64();
473 else if(
cmdline.isset(
"little-endian") ||
cmdline.isset(
"mlittle"))
477 config.ansi_c.set_arch_spec_arm(
"armhf");
481 std::string target_cpu=
486 if(!target_cpu.empty())
490 for(
auto &processor : pair.second)
491 if(processor==target_cpu)
493 if(pair.first.find(
"mips")==std::string::npos)
494 config.set_arch(pair.first);
501 if(pair.first==
"mips32o")
502 config.set_arch(
"mipsel");
503 else if(pair.first==
"mips32n")
504 config.set_arch(
"mipsn32el");
506 config.set_arch(
"mips64el");
510 if(pair.first==
"mips32o")
512 else if(pair.first==
"mips32n")
513 config.set_arch(
"mipsn32");
515 config.set_arch(
"mips64");
525 static const std::map<std::string, std::string> target_map = {
526 {
"aarch64",
"arm64" },
527 {
"aarch64_32",
"arm" },
528 {
"aarch64_be",
"none" },
532 {
"arm64_32",
"arm" },
538 {
"hexagon",
"none" },
542 {
"mips64",
"mips64" },
543 {
"mips64el",
"mips64el" },
544 {
"mipsel",
"mipsel" },
547 {
"nvptx64",
"none" },
548 {
"ppc32",
"powerpc" },
550 {
"ppc64le",
"ppc64le" },
552 {
"riscv32",
"none" },
553 {
"riscv64",
"riscv64" },
555 {
"sparcel",
"none" },
556 {
"sparcv9",
"sparc64" },
557 {
"systemz",
"none" },
559 {
"thumbeb",
"none" },
563 {
"x86_64",
"x86_64" },
566 std::string arch_quadruple =
cmdline.get_value(
"target");
568 target_map.find(arch_quadruple.substr(0, arch_quadruple.find(
'-')));
569 if(it == target_map.end())
572 config.set_arch(it->second);
576 if(
cmdline.isset(
"fshort-wchar"))
578 config.ansi_c.wchar_t_width=
config.ansi_c.short_int_width;
579 config.ansi_c.wchar_t_is_unsigned=
true;
584 if(
cmdline.isset(
"-fsingle-precision-constant"))
585 config.ansi_c.single_precision_constant=
true;
588 if(
cmdline.isset(
"fshort-double"))
594 switch(compiler.
mode)
609 log.debug() <<
"Compiling and linking a library" <<
messaget::eom;
612 log.debug() <<
"Compiling and linking an executable" <<
messaget::eom;
616 if(
cmdline.isset(
"i386-win32") ||
621 log.debug() <<
"Enabling Visual Studio syntax" <<
messaget::eom;
638 std::string std_string=
cmdline.get_value(
"std");
640 if(std_string==
"gnu89" || std_string==
"c89")
643 if(std_string==
"gnu99" || std_string==
"c99" || std_string==
"iso9899:1999" ||
644 std_string==
"gnu9x" || std_string==
"c9x" || std_string==
"iso9899:199x")
647 if(std_string==
"gnu11" || std_string==
"c11" ||
648 std_string==
"gnu1x" || std_string==
"c1x")
651 if(std_string==
"c++11" || std_string==
"c++1x" ||
652 std_string==
"gnu++11" || std_string==
"gnu++1x" ||
653 std_string==
"c++1y" ||
654 std_string==
"gnu++1y")
657 if(std_string==
"gnu++14" || std_string==
"c++14")
660 if(std_string ==
"gnu++17" || std_string ==
"c++17")
670 if(
cmdline.isset(
"short-wchar"))
671 config.ansi_c.wchar_t_width=16;
674 if(
cmdline.isset(
"short-double"))
675 config.ansi_c.double_width=32;
678 if(
cmdline.isset(
"funsigned-char"))
679 config.ansi_c.char_is_unsigned=
true;
681 if(
cmdline.isset(
"fsigned-char"))
682 config.ansi_c.char_is_unsigned=
false;
688 config.ansi_c.preprocessor_options.push_back(
"-undef");
691 config.ansi_c.preprocessor_options.push_back(
"-nostdinc");
721 std::vector<temp_dirt> temp_dirs;
724 std::string language;
726 for(goto_cc_cmdlinet::parsed_argvt::iterator
727 arg_it=
cmdline.parsed_argv.begin();
728 arg_it!=
cmdline.parsed_argv.end();
731 if(arg_it->is_infile_name)
735 if(language==
"cpp-output" || language==
"c++-cpp-output")
740 language ==
"c" || language ==
"c++" ||
743 std::string new_suffix;
747 else if(language==
"c++")
750 new_suffix=
has_suffix(arg_it->arg,
".c")?
".i":
".ii";
752 std::string new_name=
755 temp_dirs.emplace_back(
"goto-cc-XXXXXX");
756 std::string dest = temp_dirs.back()(new_name);
759 preprocess(language, arg_it->arg, dest, act_as_bcc);
772 else if(arg_it->arg==
"-x")
775 if(arg_it!=
cmdline.parsed_argv.end())
777 language=arg_it->arg;
784 language=std::string(arg_it->arg, 2, std::string::npos);
795 log.error() <<
"cannot specify -o with -c with multiple files"
824 const std::string &language,
825 const std::string &src,
826 const std::string &dest,
830 std::vector<std::string> new_argv;
832 new_argv.reserve(
cmdline.parsed_argv.size());
834 bool skip_next=
false;
836 for(goto_cc_cmdlinet::parsed_argvt::const_iterator
837 it=
cmdline.parsed_argv.begin();
846 else if(it->is_infile_name)
850 else if(it->arg==
"-c" || it->arg==
"-E" || it->arg==
"-S")
854 else if(it->arg==
"-o")
863 new_argv.push_back(it->arg);
867 new_argv.push_back(
"-E");
870 std::string stdout_file;
875 new_argv.push_back(
"-o");
876 new_argv.push_back(dest);
880 if(!language.empty())
882 new_argv.push_back(
"-x");
883 new_argv.push_back(language);
887 new_argv.push_back(src);
890 INVARIANT(new_argv.size()>=1,
"No program name in argv");
894 log.
debug() <<
"RUN:";
895 for(std::size_t i=0; i<new_argv.size(); i++)
896 log.debug() <<
" " << new_argv[i];
899 return run(new_argv[0], new_argv,
cmdline.stdin_file, stdout_file,
"");
907 std::vector<std::string> new_argv;
908 new_argv.reserve(
cmdline.parsed_argv.size());
909 for(
const auto &a :
cmdline.parsed_argv)
910 new_argv.push_back(a.arg);
915 std::map<irep_idt, std::size_t> arities;
917 for(
const auto &pair : arities)
919 std::ostringstream addition;
920 addition <<
"-D" <<
id2string(pair.first) <<
"(";
921 std::vector<char> params(pair.second);
922 std::iota(params.begin(), params.end(),
'a');
923 for(std::vector<char>::iterator it=params.begin(); it!=params.end(); ++it)
926 if(it+1!=params.end())
930 new_argv.push_back(addition.str());
938 log.
debug() <<
"RUN:";
939 for(std::size_t i=0; i<new_argv.size(); i++)
940 log.debug() <<
" " << new_argv[i];
943 return run(new_argv[0], new_argv,
cmdline.stdin_file,
"",
"");
949 bool have_files=
false;
951 for(goto_cc_cmdlinet::parsed_argvt::const_iterator
952 it=
cmdline.parsed_argv.begin();
955 if(it->is_infile_name)
962 std::list<std::string> output_files;
969 output_files.push_back(
cmdline.get_value(
'o'));
973 for(goto_cc_cmdlinet::parsed_argvt::const_iterator
974 i_it=
cmdline.parsed_argv.begin();
975 i_it!=
cmdline.parsed_argv.end();
977 if(i_it->is_infile_name &&
986 output_files.push_back(
cmdline.get_value(
'o'));
988 output_files.push_back(
"a.out");
991 if(output_files.empty() ||
992 (output_files.size()==1 &&
993 output_files.front()==
"/dev/null"))
1001 std::list<std::string> goto_binaries;
1002 for(std::list<std::string>::const_iterator
1003 it=output_files.begin();
1004 it!=output_files.end();
1011 std::filesystem::rename(*it, bin_name);
1013 catch(
const std::filesystem::filesystem_error &e)
1015 log.error() <<
"Rename failed: " << e.what() <<
messaget::eom;
1019 goto_binaries.push_back(bin_name);
1026 goto_binaries.size()==1 &&
1027 output_files.size()==1)
1030 output_files.front(),
1031 goto_binaries.front(),
1037 std::string native_tool;
1046 for(std::list<std::string>::const_iterator
1047 it=output_files.begin();
1048 it!=output_files.end();
1067 const std::list<std::string> &preprocessed_source_files,
1071 bool have_files=
false;
1073 for(goto_cc_cmdlinet::parsed_argvt::const_iterator
1074 it=
cmdline.parsed_argv.begin();
1075 it!=
cmdline.parsed_argv.end();
1077 if(it->is_infile_name)
1097 std::map<std::string, std::string> output_files;
1102 for(
const auto &s : preprocessed_source_files)
1103 output_files.insert(std::make_pair(s,
cmdline.get_value(
'o')));
1107 for(
const std::string &s : preprocessed_source_files)
1108 output_files.insert(
1112 if(output_files.empty() ||
1113 (output_files.size()==1 &&
1114 output_files.begin()->second==
"/dev/null"))
1117 log.
debug() <<
"Appending preprocessed sources to generate hybrid asm output"
1120 for(
const auto &so : output_files)
1122 std::ifstream is(so.first);
1125 log.error() <<
"Failed to open input source " << so.first
1130 std::ofstream os(so.second, std::ios::app);
1133 log.error() <<
"Failed to open output file " << so.second
1138 const char comment=act_as_bcc ?
':' :
'#';
1144 while(std::getline(is, line))
1156 std::cout <<
"goto-cc understands the options of "
1157 <<
"gcc plus the following.\n\n";
std::string get_value(char option) const
virtual bool isset(char option) const
@ COMPILE_LINK_EXECUTABLE
std::string output_file_object
bool add_input_file(const std::string &)
puts input file names into a list and does preprocessing for libraries.
std::list< std::string > libraries
void cprover_macro_arities(std::map< irep_idt, std::size_t > &cprover_macros) const
__CPROVER_... macros written to object files and their arities
std::list< std::string > object_files
bool doit()
reads and source and object files, compiles and links them into goto program objects.
std::list< std::string > source_files
bool wrote_object_files() const
Has this compiler written any object files?
std::string object_file_extension
enum compilet::@010007010156070135133373264143331307343141370152 mode
std::list< std::string > library_paths
std::string output_file_executable
std::string native_tool_name
int preprocess(const std::string &language, const std::string &src, const std::string &dest, bool act_as_bcc)
call gcc for preprocessing
gcc_modet(goto_cc_cmdlinet &_cmdline, const std::string &_base_name, bool _produce_hybrid_binary)
static bool needs_preprocessing(const std::string &)
const std::string goto_binary_tmp_suffix
int run_gcc(const compilet &compiler)
call gcc with original command line
gcc_message_handlert gcc_message_handler
void help_mode() final
display command line help
const std::map< std::string, std::set< std::string > > arch_map
Associate CBMC architectures with processor names.
const bool produce_hybrid_binary
int asm_output(bool act_as_bcc, const std::list< std::string > &preprocessed_source_files, const compilet &compiler)
int gcc_hybrid_binary(compilet &compiler)
goto_cc_modet(goto_cc_cmdlinet &, const std::string &_base_name, message_handlert &)
constructor
goto_cc_cmdlinet & cmdline
const std::string base_name
void help()
display command line help
Synthesise definitions of symbols that are defined in linker scripts.
int add_linker_script_definitions()
Add values of linkerscript-defined symbols to the goto-binary.
Class that provides messages with a built-in verbosity 'level'.
static unsigned eval_verbosity(const std::string &user_input, const message_levelt default_verbosity, message_handlert &dest)
Parse a (user-)provided string as a verbosity level and set it as the verbosity of dest.
Compile and link source and object files.
bool has_prefix(const std::string &s, const std::string &prefix)
static std::string linker_name(const cmdlinet &cmdline, const std::string &base_name)
static std::string compiler_name(const cmdlinet &cmdline, const std::string &base_name)
Base class for command line interpretation.
void configure_gcc(const gcc_versiont &gcc_version)
std::string get_base_name(const std::string &in, bool strip_suffix)
cleans a filename from path and extension
Command line interpretation for goto-cc.
int hybrid_binary(const std::string &compiler_or_linker, const std::string &goto_binary_file, const std::string &output_file, bool building_executable, message_handlert &message_handler, bool linking_efi)
Merges a goto binary into an object file (e.g.
Create hybrid binary with goto-binary section.
const std::string & id2string(const irep_idt &d)
Merge linker script-defined symbols into a goto-program.
static std::string comment(const rw_set_baset::entryt &entry, bool write)
int run(const std::string &what, const std::vector< std::string > &argv)
#define PRECONDITION(CONDITION)
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
bool has_suffix(const std::string &s, const std::string &suffix)
const char * CBMC_VERSION