Go to the documentation of this file.
17 #define EX_SOFTWARE 70
55 const std::string &base_name)
57 if(cmdline.
isset(
"native-compiler"))
58 return cmdline.
get_value(
"native-compiler");
60 if(base_name==
"bcc" ||
61 base_name.find(
"goto-bcc")!=std::string::npos)
64 if(base_name==
"goto-clang")
69 if(
pos==std::string::npos ||
70 base_name==
"goto-gcc" ||
80 std::string result=base_name;
81 result.replace(
pos, 8,
"gcc");
88 const std::string &base_name)
90 if(cmdline.
isset(
"native-linker"))
91 return cmdline.
get_value(
"native-linker");
95 if(
pos==std::string::npos ||
96 base_name==
"goto-gcc" ||
100 std::string result=base_name;
101 result.replace(
pos, 7,
"ld");
108 const std::string &_base_name,
109 bool _produce_hybrid_binary):
111 produce_hybrid_binary(_produce_hybrid_binary),
112 goto_binary_tmp_suffix(
".goto-cc-saved"),
132 "strongarm",
"strongarm110",
"strongarm1100",
"strongarm1110",
133 "arm2",
"arm250",
"arm3",
"arm6",
"arm60",
"arm600",
"arm610",
134 "arm620",
"fa526",
"fa626",
"fa606te",
"fa626te",
"fmp626",
135 "xscale",
"iwmmxt",
"iwmmxt2",
"xgene1"
138 "armv7",
"arm7m",
"arm7d",
"arm7dm",
"arm7di",
"arm7dmi",
139 "arm70",
"arm700",
"arm700i",
"arm710",
"arm710c",
"arm7100",
140 "arm720",
"arm7500",
"arm7500fe",
"arm7tdmi",
"arm7tdmi-s",
141 "arm710t",
"arm720t",
"arm740t",
"mpcore",
"mpcorenovfp",
142 "arm8",
"arm810",
"arm9",
"arm9e",
"arm920",
"arm920t",
143 "arm922t",
"arm946e-s",
"arm966e-s",
"arm968e-s",
"arm926ej-s",
144 "arm940t",
"arm9tdmi",
"arm10tdmi",
"arm1020t",
"arm1026ej-s",
145 "arm10e",
"arm1020e",
"arm1022e",
"arm1136j-s",
"arm1136jf-s",
146 "arm1156t2-s",
"arm1156t2f-s",
"arm1176jz-s",
"arm1176jzf-s",
147 "cortex-a5",
"cortex-a7",
"cortex-a8",
"cortex-a9",
148 "cortex-a12",
"cortex-a15",
"cortex-a53",
"cortex-r4",
149 "cortex-r4f",
"cortex-r5",
"cortex-r7",
"cortex-m7",
150 "cortex-m4",
"cortex-m3",
"cortex-m1",
"cortex-m0",
151 "cortex-m0plus",
"cortex-m1.small-multiply",
152 "cortex-m0.small-multiply",
"cortex-m0plus.small-multiply",
153 "marvell-pj4",
"ep9312",
"fa726te",
156 "cortex-a57",
"cortex-a72",
"exynos-m1"
158 {
"hppa", {
"1.0",
"1.1",
"2.0"}},
163 "powerpc",
"601",
"602",
"603",
"603e",
"604",
"604e",
"630",
167 "G4",
"7400",
"7450",
169 "401",
"403",
"405",
"405fp",
"440",
"440fp",
"464",
"464fp",
173 "e300c2",
"e300c3",
"e500mc",
"ec603e",
186 "power3",
"power4",
"power5",
"power5+",
"power6",
"power6x",
190 "e500mc64",
"e5500",
"e6500",
195 {
"powerpc64le", {
"powerpc64le",
"power8"}},
217 "loongson2e",
"loongson2f",
"loongson3a",
"mips64",
"mips64r2",
218 "mips64r3",
"mips64r5",
"mips64r6 4kc",
"5kc",
"5kf",
"20kc",
219 "octeon",
"octeon+",
"octeon2",
"octeon3",
"sb1",
"vr4100",
220 "vr4111",
"vr4120",
"vr4130",
"vr4300",
"vr5000",
"vr5400",
221 "vr5500",
"sr71000",
"xlp",
224 "mips32",
"mips32r2",
"mips32r3",
"mips32r5",
"mips32r6",
226 "4km",
"4kp",
"4ksc",
"4kec",
"4kem",
"4kep",
"4ksd",
"24kc",
227 "24kf2_1",
"24kf1_1",
"24kec",
"24kef2_1",
"24kef1_1",
"34kc",
228 "34kf2_1",
"34kf1_1",
"34kn",
"74kc",
"74kf2_1",
"74kf1_1",
229 "74kf3_2",
"1004kc",
"1004kf2_1",
"1004kf1_1",
"m4k",
"m14k",
230 "m14kc",
"m14ke",
"m14kec",
235 "mips1",
"mips2",
"r2000",
"r3000",
239 "mips3",
"mips4",
"r4000",
"r4400",
"r4600",
"r4650",
"r4700",
240 "r8000",
"rm7000",
"rm9000",
"r10000",
"r12000",
"r14000",
251 "z900",
"z990",
"g5",
"g6",
254 "z9-109",
"z9-ec",
"z10",
"z196",
"zEC12",
"z13"
262 "v7",
"v8",
"leon",
"leon3",
"leon3v7",
"cypress",
"supersparc",
263 "hypersparc",
"sparclite",
"f930",
"f934",
"sparclite86x",
267 "v9",
"ultrasparc",
"ultrasparc3",
"niagara",
"niagara2",
268 "niagara3",
"niagara4",
271 "itanium",
"itanium1",
"merced",
"itanium2",
"mckinley"
278 "i386",
"i486",
"i586",
"i686",
280 "k6",
"k6-2",
"k6-3",
"athlon" "athlon-tbird",
"athlon-4",
281 "athlon-xp",
"athlon-mp",
284 "pentium",
"pentium-mmx",
"pentiumpro" "pentium2",
"pentium3",
285 "pentium3m",
"pentium-m" "pentium4",
"pentium4m",
"prescott",
287 "winchip-c6",
"winchip2",
"c3",
"c3-2",
"geode",
291 "nocona",
"core2",
"nehalem" "westmere",
"sandybridge",
"knl",
292 "ivybridge",
"haswell",
"broadwell" "bonnell",
"silvermont",
294 "k8",
"k8-sse3",
"opteron",
"athlon64",
"athlon-fx",
295 "opteron-sse3" "athlon64-sse3",
"amdfam10",
"barcelona",
297 "bdver1",
"bdver2" "bdver3",
"bdver4",
339 base_name.find(
"goto-bcc")!=std::string::npos;
351 std::cout <<
"bcc: version " <<
gcc_version <<
" (goto-cc "
356 std::cout <<
"clang version " <<
gcc_version <<
" (goto-cc "
377 <<
"Copyright (C) 2006-2018 Daniel Kroening, Christoph Wintersteiger\n"
414 debug() <<
"BCC mode (hybrid)" <<
eom;
421 debug() <<
"GCC mode (hybrid)" <<
eom;
482 std::string target_cpu=
487 if(!target_cpu.empty())
491 for(
auto &processor : pair.second)
492 if(processor==target_cpu)
494 if(pair.first.find(
"mips")==std::string::npos)
502 if(pair.first==
"mips32o")
504 else if(pair.first==
"mips32n")
511 if(pair.first==
"mips32o")
513 else if(pair.first==
"mips32n")
541 switch(compiler.
mode)
544 debug() <<
"Linking a library only" <<
eom;
break;
546 debug() <<
"Compiling only" <<
eom;
break;
548 debug() <<
"Assembling only" <<
eom;
break;
550 debug() <<
"Preprocessing only" <<
eom;
break;
552 debug() <<
"Compiling and linking a library" <<
eom;
break;
554 debug() <<
"Compiling and linking an executable" <<
eom;
break;
562 debug() <<
"Enabling Visual Studio syntax" <<
eom;
581 if(std_string==
"gnu89" || std_string==
"c89")
584 if(std_string==
"gnu99" || std_string==
"c99" || std_string==
"iso9899:1999" ||
585 std_string==
"gnu9x" || std_string==
"c9x" || std_string==
"iso9899:199x")
588 if(std_string==
"gnu11" || std_string==
"c11" ||
589 std_string==
"gnu1x" || std_string==
"c1x")
592 if(std_string==
"c++11" || std_string==
"c++1x" ||
593 std_string==
"gnu++11" || std_string==
"gnu++1x" ||
594 std_string==
"c++1y" ||
595 std_string==
"gnu++1y")
598 if(std_string==
"gnu++14" || std_string==
"c++14")
662 std::string language;
664 for(goto_cc_cmdlinet::parsed_argvt::iterator
669 if(arg_it->is_infile_name)
673 if(language==
"cpp-output" || language==
"c++-cpp-output")
678 language ==
"c" || language ==
"c++" ||
681 std::string new_suffix;
685 else if(language==
"c++")
688 new_suffix=
has_suffix(arg_it->arg,
".c")?
".i":
".ii";
690 std::string new_name=
692 std::string dest=temp_dir(new_name);
695 preprocess(language, arg_it->arg, dest, act_as_bcc);
699 error() <<
"preprocessing has failed" <<
eom;
708 else if(arg_it->arg==
"-x")
713 language=arg_it->arg;
720 language=std::string(arg_it->arg, 2, std::string::npos);
731 error() <<
"cannot specify -o with -c with multiple files" <<
eom;
759 const std::string &language,
760 const std::string &src,
761 const std::string &dest,
765 std::vector<std::string> new_argv;
769 bool skip_next=
false;
771 for(goto_cc_cmdlinet::parsed_argvt::const_iterator
781 else if(it->is_infile_name)
785 else if(it->arg==
"-c" || it->arg==
"-E" || it->arg==
"-S")
789 else if(it->arg==
"-o")
798 new_argv.push_back(it->arg);
802 new_argv.push_back(
"-E");
805 std::string stdout_file;
810 new_argv.push_back(
"-o");
811 new_argv.push_back(dest);
815 if(!language.empty())
817 new_argv.push_back(
"-x");
818 new_argv.push_back(language);
822 new_argv.push_back(src);
825 INVARIANT(new_argv.size()>=1,
"No program name in argv");
829 for(std::size_t i=0; i<new_argv.size(); i++)
830 debug() <<
" " << new_argv[i];
841 std::vector<std::string> new_argv;
844 new_argv.push_back(a.arg);
849 std::map<irep_idt, std::size_t> arities;
851 for(
const auto &pair : arities)
853 std::ostringstream addition;
854 addition <<
"-D" <<
id2string(pair.first) <<
"(";
855 std::vector<char> params(pair.second);
856 std::iota(params.begin(), params.end(),
'a');
857 for(std::vector<char>::iterator it=params.begin(); it!=params.end(); ++it)
860 if(it+1!=params.end())
864 new_argv.push_back(addition.str());
872 for(std::size_t i=0; i<new_argv.size(); i++)
873 debug() <<
" " << new_argv[i];
882 bool have_files=
false;
884 for(goto_cc_cmdlinet::parsed_argvt::const_iterator
888 if(it->is_infile_name)
895 std::list<std::string> output_files;
906 for(goto_cc_cmdlinet::parsed_argvt::const_iterator
910 if(i_it->is_infile_name &&
921 output_files.push_back(
"a.out");
924 if(output_files.empty() ||
925 (output_files.size()==1 &&
926 output_files.front()==
"/dev/null"))
930 <<
" to generate hybrid binary" <<
eom;
933 std::list<std::string> goto_binaries;
934 for(std::list<std::string>::const_iterator
935 it=output_files.begin();
936 it!=output_files.end();
940 int result=rename(it->c_str(), bin_name.c_str());
943 error() <<
"Rename failed: " << std::strerror(errno) <<
eom;
946 goto_binaries.push_back(bin_name);
953 goto_binaries.size()==1 &&
954 output_files.size()==1)
957 compiler, output_files.front(), goto_binaries.front(),
962 std::string native_tool;
971 for(std::list<std::string>::const_iterator
972 it=output_files.begin();
973 it!=output_files.end();
992 const std::list<std::string> &preprocessed_source_files,
996 bool have_files=
false;
998 for(goto_cc_cmdlinet::parsed_argvt::const_iterator
1002 if(it->is_infile_name)
1012 <<
" to generate native asm output" <<
eom;
1020 std::map<std::string, std::string> output_files;
1025 for(
const auto &s : preprocessed_source_files)
1030 for(
const std::string &s : preprocessed_source_files)
1031 output_files.insert(
1035 if(output_files.empty() ||
1036 (output_files.size()==1 &&
1037 output_files.begin()->second==
"/dev/null"))
1041 <<
"Appending preprocessed sources to generate hybrid asm output"
1044 for(
const auto &so : output_files)
1046 std::ifstream is(so.first);
1049 error() <<
"Failed to open input source " << so.first <<
eom;
1053 std::ofstream os(so.second, std::ios::app);
1056 error() <<
"Failed to open output file " << so.second <<
eom;
1060 const char comment=act_as_bcc ?
':' :
'#';
1066 while(std::getline(is, line))
1078 std::cout <<
"goto-cc understands the options of "
1079 <<
"gcc plus the following.\n\n";
const char * CBMC_VERSION
int gcc_hybrid_binary(compilet &compiler)
std::string get_base_name(const std::string &in, bool strip_suffix)
cleans a filename from path and extension
void get(const std::string &executable)
Merge linker script-defined symbols into a goto-program.
virtual bool isset(char option) const
std::list< std::string > source_files
std::size_t wchar_t_width
static std::string compiler_name(const cmdlinet &cmdline, const std::string &base_name)
int add_linker_script_definitions()
Add values of linkerscript-defined symbols to the goto-binary.
void help_mode() final
display command line help
bool doit()
reads and source and object files, compiles and links them into goto program objects.
void configure_gcc(const gcc_versiont &gcc_version)
enum gcc_versiont::flavort flavor
void set_arch_spec_i386()
int run(const std::string &what, const std::vector< std::string > &argv)
std::list< std::string > libraries
Synthesise definitions of symbols that are defined in linker scripts.
const std::string base_name
std::string native_tool_name
std::list< std::string > undefines
struct configt::ansi_ct ansi_c
bool has_suffix(const std::string &s, const std::string &suffix)
static bool needs_preprocessing(const std::string &)
configt::cppt::cpp_standardt default_cxx_standard
bool wrote_object_files() const
Has this compiler written any object files?
std::string output_file_object
std::list< std::string > object_files
mstreamt & result() const
void set_arch_spec_arm(const irep_idt &subarch)
const std::string & id2string(const irep_idt &d)
int run_gcc(const compilet &compiler)
call gcc with original command line
@ COMPILE_LINK_EXECUTABLE
std::string output_file_executable
const std::map< std::string, std::set< std::string > > arch_map
Associate CBMC architectures with processor names.
#define PRECONDITION(CONDITION)
std::string get_value(char option) const
const std::string goto_binary_tmp_suffix
std::list< std::string > library_paths
static irep_idt this_operating_system()
const bool produce_hybrid_binary
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)
Merges a goto binary into an object file (e.g.
std::string object_file_extension
goto_cc_cmdlinet & cmdline
int asm_output(bool act_as_bcc, const std::list< std::string > &preprocessed_source_files, const compilet &compiler)
std::list< std::string > preprocessor_options
bool have_infile_arg() const
gcc_message_handlert gcc_message_handler
bool add_input_file(const std::string &)
puts input file names into a list and does preprocessing for libraries.
static irep_idt this_architecture()
int preprocess(const std::string &language, const std::string &src, const std::string &dest, bool act_as_bcc)
call gcc for preprocessing
message_handlert & get_message_handler()
bool set(const cmdlinet &cmdline)
enum configt::ansi_ct::c_standardt c_standard
configt::ansi_ct::c_standardt default_c_standard
std::size_t short_int_width
void set_arch_spec_x86_64()
bool has_prefix(const std::string &s, const std::string &prefix)
virtual void help()
display command line help
unsignedbv_typet size_type()
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.
bool single_precision_constant
const std::list< std::string > & get_values(const std::string &option) const
static std::string comment(const rw_set_baset::entryt &entry, bool write)
static std::string linker_name(const cmdlinet &cmdline, const std::string &base_name)
void set_arch(const irep_idt &)
void cprover_macro_arities(std::map< irep_idt, std::size_t > &cprover_macros) const
__CPROVER_... macros written to object files and their arities
gcc_modet(goto_cc_cmdlinet &_cmdline, const std::string &_base_name, bool _produce_hybrid_binary)
enum configt::cppt::cpp_standardt cpp_standard