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 "
376 <<
"Copyright (C) 2006-2018 Daniel Kroening, Christoph Wintersteiger\n"
413 debug() <<
"BCC mode (hybrid)" <<
eom;
420 debug() <<
"GCC mode (hybrid)" <<
eom;
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)
501 if(pair.first==
"mips32o")
503 else if(pair.first==
"mips32n")
510 if(pair.first==
"mips32o")
512 else if(pair.first==
"mips32n")
540 switch(compiler.
mode)
543 debug() <<
"Linking a library only" <<
eom;
break;
545 debug() <<
"Compiling only" <<
eom;
break;
547 debug() <<
"Assembling only" <<
eom;
break;
549 debug() <<
"Preprocessing only" <<
eom;
break;
551 debug() <<
"Compiling and linking a library" <<
eom;
break;
553 debug() <<
"Compiling and linking an executable" <<
eom;
break;
561 debug() <<
"Enabling Visual Studio syntax" <<
eom;
580 if(std_string==
"gnu89" || std_string==
"c89")
583 if(std_string==
"gnu99" || std_string==
"c99" || std_string==
"iso9899:1999" ||
584 std_string==
"gnu9x" || std_string==
"c9x" || std_string==
"iso9899:199x")
587 if(std_string==
"gnu11" || std_string==
"c11" ||
588 std_string==
"gnu1x" || std_string==
"c1x")
591 if(std_string==
"c++11" || std_string==
"c++1x" ||
592 std_string==
"gnu++11" || std_string==
"gnu++1x" ||
593 std_string==
"c++1y" ||
594 std_string==
"gnu++1y")
597 if(std_string==
"gnu++14" || std_string==
"c++14")
658 std::vector<temp_dirt> temp_dirs;
661 std::string language;
663 for(goto_cc_cmdlinet::parsed_argvt::iterator
668 if(arg_it->is_infile_name)
672 if(language==
"cpp-output" || language==
"c++-cpp-output")
677 language ==
"c" || language ==
"c++" ||
680 std::string new_suffix;
684 else if(language==
"c++")
687 new_suffix=
has_suffix(arg_it->arg,
".c")?
".i":
".ii";
689 std::string new_name=
692 temp_dirs.emplace_back(
"goto-cc-XXXXXX");
693 std::string dest = temp_dirs.back()(new_name);
696 preprocess(language, arg_it->arg, dest, act_as_bcc);
700 error() <<
"preprocessing has failed" <<
eom;
709 else if(arg_it->arg==
"-x")
714 language=arg_it->arg;
721 language=std::string(arg_it->arg, 2, std::string::npos);
732 error() <<
"cannot specify -o with -c with multiple files" <<
eom;
760 const std::string &language,
761 const std::string &src,
762 const std::string &dest,
766 std::vector<std::string> new_argv;
770 bool skip_next=
false;
772 for(goto_cc_cmdlinet::parsed_argvt::const_iterator
782 else if(it->is_infile_name)
786 else if(it->arg==
"-c" || it->arg==
"-E" || it->arg==
"-S")
790 else if(it->arg==
"-o")
799 new_argv.push_back(it->arg);
803 new_argv.push_back(
"-E");
806 std::string stdout_file;
811 new_argv.push_back(
"-o");
812 new_argv.push_back(dest);
816 if(!language.empty())
818 new_argv.push_back(
"-x");
819 new_argv.push_back(language);
823 new_argv.push_back(src);
826 INVARIANT(new_argv.size()>=1,
"No program name in argv");
830 for(std::size_t i=0; i<new_argv.size(); i++)
831 debug() <<
" " << new_argv[i];
842 std::vector<std::string> new_argv;
845 new_argv.push_back(a.arg);
850 std::map<irep_idt, std::size_t> arities;
852 for(
const auto &pair : arities)
854 std::ostringstream addition;
855 addition <<
"-D" <<
id2string(pair.first) <<
"(";
856 std::vector<char> params(pair.second);
857 std::iota(params.begin(), params.end(),
'a');
858 for(std::vector<char>::iterator it=params.begin(); it!=params.end(); ++it)
861 if(it+1!=params.end())
865 new_argv.push_back(addition.str());
873 for(std::size_t i=0; i<new_argv.size(); i++)
874 debug() <<
" " << new_argv[i];
883 bool have_files=
false;
885 for(goto_cc_cmdlinet::parsed_argvt::const_iterator
889 if(it->is_infile_name)
896 std::list<std::string> output_files;
907 for(goto_cc_cmdlinet::parsed_argvt::const_iterator
911 if(i_it->is_infile_name &&
922 output_files.push_back(
"a.out");
925 if(output_files.empty() ||
926 (output_files.size()==1 &&
927 output_files.front()==
"/dev/null"))
931 <<
" to generate hybrid binary" <<
eom;
934 std::list<std::string> goto_binaries;
935 for(std::list<std::string>::const_iterator
936 it=output_files.begin();
937 it!=output_files.end();
952 goto_binaries.push_back(bin_name);
959 goto_binaries.size()==1 &&
960 output_files.size()==1)
963 compiler, output_files.front(), goto_binaries.front(),
968 std::string native_tool;
977 for(std::list<std::string>::const_iterator
978 it=output_files.begin();
979 it!=output_files.end();
998 const std::list<std::string> &preprocessed_source_files,
1002 bool have_files=
false;
1004 for(goto_cc_cmdlinet::parsed_argvt::const_iterator
1008 if(it->is_infile_name)
1018 <<
" to generate native asm output" <<
eom;
1026 std::map<std::string, std::string> output_files;
1031 for(
const auto &s : preprocessed_source_files)
1036 for(
const std::string &s : preprocessed_source_files)
1037 output_files.insert(
1041 if(output_files.empty() ||
1042 (output_files.size()==1 &&
1043 output_files.begin()->second==
"/dev/null"))
1047 <<
"Appending preprocessed sources to generate hybrid asm output"
1050 for(
const auto &so : output_files)
1052 std::ifstream is(so.first);
1055 error() <<
"Failed to open input source " << so.first <<
eom;
1059 std::ofstream os(so.second, std::ios::app);
1062 error() <<
"Failed to open output file " << so.second <<
eom;
1066 const char comment=act_as_bcc ?
':' :
'#';
1072 while(std::getline(is, line))
1084 std::cout <<
"goto-cc understands the options of "
1085 <<
"gcc plus the following.\n\n";
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?
const char * CBMC_VERSION
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
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)
virtual std::string what() const =0
A human readable description of what went wrong.
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
@ COMPILE_LINK_EXECUTABLE
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.
Create hybrid binary with goto-binary section.
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)
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
Base class for exceptions thrown in the cprover project.
Base class for command line interpretation.
void file_rename(const std::string &old_path, const std::string &new_path)
Rename a file.
gcc_modet(goto_cc_cmdlinet &_cmdline, const std::string &_base_name, bool _produce_hybrid_binary)
enum configt::cppt::cpp_standardt cpp_standard