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;
479 std::string target_cpu=
488 for(
auto &processor : pair.second)
489 if(processor==target_cpu)
491 if(pair.first.find(
"mips")==std::string::npos)
499 if(pair.first==
"mips32o")
501 else if(pair.first==
"mips32n")
508 if(pair.first==
"mips32o")
510 else if(pair.first==
"mips32n")
536 const auto gcc_float128_minor_version =
547 switch(compiler.
mode)
550 debug() <<
"Linking a library only" <<
eom;
break;
552 debug() <<
"Compiling only" <<
eom;
break;
554 debug() <<
"Assembling only" <<
eom;
break;
556 debug() <<
"Preprocessing only" <<
eom;
break;
558 debug() <<
"Compiling and linking a library" <<
eom;
break;
560 debug() <<
"Compiling and linking an executable" <<
eom;
break;
568 debug() <<
"Enabling Visual Studio syntax" <<
eom;
587 if(std_string==
"gnu89" || std_string==
"c89")
590 if(std_string==
"gnu99" || std_string==
"c99" || std_string==
"iso9899:1999" ||
591 std_string==
"gnu9x" || std_string==
"c9x" || std_string==
"iso9899:199x")
594 if(std_string==
"gnu11" || std_string==
"c11" ||
595 std_string==
"gnu1x" || std_string==
"c1x")
598 if(std_string==
"c++11" || std_string==
"c++1x" ||
599 std_string==
"gnu++11" || std_string==
"gnu++1x" ||
600 std_string==
"c++1y" ||
601 std_string==
"gnu++1y")
604 if(std_string==
"gnu++14" || std_string==
"c++14")
668 std::string language;
670 for(goto_cc_cmdlinet::parsed_argvt::iterator
675 if(arg_it->is_infile_name)
679 if(language==
"cpp-output" || language==
"c++-cpp-output")
683 else if(language==
"c" || language==
"c++" ||
686 std::string new_suffix;
690 else if(language==
"c++")
693 new_suffix=
has_suffix(arg_it->arg,
".c")?
".i":
".ii";
695 std::string new_name=
697 std::string dest=temp_dir(new_name);
700 preprocess(language, arg_it->arg, dest, act_as_bcc);
704 error() <<
"preprocessing has failed" <<
eom;
713 else if(arg_it->arg==
"-x")
718 language=arg_it->arg;
725 language=std::string(arg_it->arg, 2, std::string::npos);
736 error() <<
"cannot specify -o with -c with multiple files" <<
eom;
764 const std::string &language,
765 const std::string &src,
766 const std::string &dest,
770 std::vector<std::string> new_argv;
774 bool skip_next=
false;
776 for(goto_cc_cmdlinet::parsed_argvt::const_iterator
786 else if(it->is_infile_name)
790 else if(it->arg==
"-c" || it->arg==
"-E" || it->arg==
"-S")
794 else if(it->arg==
"-o")
803 new_argv.push_back(it->arg);
807 new_argv.push_back(
"-E");
810 std::string stdout_file;
815 new_argv.push_back(
"-o");
816 new_argv.push_back(dest);
822 new_argv.push_back(
"-x");
823 new_argv.push_back(language);
827 new_argv.push_back(src);
830 INVARIANT(new_argv.size()>=1,
"No program name in argv");
834 for(std::size_t i=0; i<new_argv.size(); i++)
835 debug() <<
" " << new_argv[i];
846 std::vector<std::string> new_argv;
849 new_argv.push_back(a.arg);
854 std::map<irep_idt, std::size_t> arities;
856 for(
const auto &pair : arities)
858 std::ostringstream addition;
859 addition <<
"-D" <<
id2string(pair.first) <<
"(";
860 std::vector<char> params(pair.second);
861 std::iota(params.begin(), params.end(),
'a');
862 for(std::vector<char>::iterator it=params.begin(); it!=params.end(); ++it)
865 if(it+1!=params.end())
869 new_argv.push_back(addition.str());
877 for(std::size_t i=0; i<new_argv.size(); i++)
878 debug() <<
" " << new_argv[i];
887 bool have_files=
false;
889 for(goto_cc_cmdlinet::parsed_argvt::const_iterator
893 if(it->is_infile_name)
900 std::list<std::string> output_files;
911 for(goto_cc_cmdlinet::parsed_argvt::const_iterator
915 if(i_it->is_infile_name &&
926 output_files.push_back(
"a.out");
929 if(output_files.empty() ||
930 (output_files.size()==1 &&
931 output_files.front()==
"/dev/null"))
935 <<
" to generate hybrid binary" <<
eom;
938 std::list<std::string> goto_binaries;
939 for(std::list<std::string>::const_iterator
940 it=output_files.begin();
941 it!=output_files.end();
945 int result=rename(it->c_str(), bin_name.c_str());
948 error() <<
"Rename failed: " << std::strerror(errno) <<
eom;
951 goto_binaries.push_back(bin_name);
958 goto_binaries.size()==1 &&
959 output_files.size()==1)
962 compiler, output_files.front(), goto_binaries.front(),
967 std::string native_tool;
976 for(std::list<std::string>::const_iterator
977 it=output_files.begin();
978 it!=output_files.end();
993 const std::list<std::string> &preprocessed_source_files,
997 bool have_files=
false;
999 for(goto_cc_cmdlinet::parsed_argvt::const_iterator
1003 if(it->is_infile_name)
1013 <<
" to generate native asm output" <<
eom;
1021 std::map<std::string, std::string> output_files;
1026 for(
const auto &s : preprocessed_source_files)
1031 for(
const std::string &s : preprocessed_source_files)
1032 output_files.insert(
1036 if(output_files.empty() ||
1037 (output_files.size()==1 &&
1038 output_files.begin()->second==
"/dev/null"))
1042 <<
"Appending preprocessed sources to generate hybrid asm output"
1045 for(
const auto &so : output_files)
1047 std::ifstream is(so.first);
1050 error() <<
"Failed to open input source " << so.first <<
eom;
1054 std::ofstream os(so.second, std::ios::app);
1057 error() <<
"Failed to open output file " << so.second <<
eom;
1061 const char comment=act_as_bcc ?
':' :
'#';
1067 while(std::getline(is, line))
1079 std::cout <<
"goto-cc understands the options of "
1080 <<
"gcc plus the following.\n\n";
const char * CBMC_VERSION
int gcc_hybrid_binary(compilet &compiler)
bool ts_18661_3_Floatn_types
std::string get_base_name(const std::string &in, bool strip_suffix)
cleans a filename from path and extension
#define PRECONDITION(CONDITION)
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::string comment(const rw_set_baset::entryt &entry, bool write)
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.
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)
int hybrid_binary(const std::string &compiler_or_linker, const std::string &goto_binary_file, const std::string &output_file, message_handlert &message_handler)
Merges a goto binary into an object file (e.g.
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.
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
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 is_at_least(unsigned v_major, unsigned v_minor=0, unsigned v_patchlevel=0) const
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 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