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"
483 std::string target_cpu=
488 if(!target_cpu.empty())
492 for(
auto &processor : pair.second)
493 if(processor==target_cpu)
495 if(pair.first.find(
"mips")==std::string::npos)
503 if(pair.first==
"mips32o")
505 else if(pair.first==
"mips32n")
512 if(pair.first==
"mips32o")
514 else if(pair.first==
"mips32n")
542 switch(compiler.
mode)
557 log.debug() <<
"Compiling and linking a library" <<
messaget::eom;
560 log.debug() <<
"Compiling and linking an executable" <<
messaget::eom;
569 log.debug() <<
"Enabling Visual Studio syntax" <<
messaget::eom;
588 if(std_string==
"gnu89" || std_string==
"c89")
591 if(std_string==
"gnu99" || std_string==
"c99" || std_string==
"iso9899:1999" ||
592 std_string==
"gnu9x" || std_string==
"c9x" || std_string==
"iso9899:199x")
595 if(std_string==
"gnu11" || std_string==
"c11" ||
596 std_string==
"gnu1x" || std_string==
"c1x")
599 if(std_string==
"c++11" || std_string==
"c++1x" ||
600 std_string==
"gnu++11" || std_string==
"gnu++1x" ||
601 std_string==
"c++1y" ||
602 std_string==
"gnu++1y")
605 if(std_string==
"gnu++14" || std_string==
"c++14")
666 std::vector<temp_dirt> temp_dirs;
669 std::string language;
671 for(goto_cc_cmdlinet::parsed_argvt::iterator
676 if(arg_it->is_infile_name)
680 if(language==
"cpp-output" || language==
"c++-cpp-output")
685 language ==
"c" || language ==
"c++" ||
688 std::string new_suffix;
692 else if(language==
"c++")
695 new_suffix=
has_suffix(arg_it->arg,
".c")?
".i":
".ii";
697 std::string new_name=
700 temp_dirs.emplace_back(
"goto-cc-XXXXXX");
701 std::string dest = temp_dirs.back()(new_name);
704 preprocess(language, arg_it->arg, dest, act_as_bcc);
717 else if(arg_it->arg==
"-x")
722 language=arg_it->arg;
729 language=std::string(arg_it->arg, 2, std::string::npos);
740 log.error() <<
"cannot specify -o with -c with multiple files"
769 const std::string &language,
770 const std::string &src,
771 const std::string &dest,
775 std::vector<std::string> new_argv;
779 bool skip_next=
false;
781 for(goto_cc_cmdlinet::parsed_argvt::const_iterator
791 else if(it->is_infile_name)
795 else if(it->arg==
"-c" || it->arg==
"-E" || it->arg==
"-S")
799 else if(it->arg==
"-o")
808 new_argv.push_back(it->arg);
812 new_argv.push_back(
"-E");
815 std::string stdout_file;
820 new_argv.push_back(
"-o");
821 new_argv.push_back(dest);
825 if(!language.empty())
827 new_argv.push_back(
"-x");
828 new_argv.push_back(language);
832 new_argv.push_back(src);
835 INVARIANT(new_argv.size()>=1,
"No program name in argv");
839 log.debug() <<
"RUN:";
840 for(std::size_t i=0; i<new_argv.size(); i++)
841 log.debug() <<
" " << new_argv[i];
852 std::vector<std::string> new_argv;
855 new_argv.push_back(a.arg);
860 std::map<irep_idt, std::size_t> arities;
862 for(
const auto &pair : arities)
864 std::ostringstream addition;
865 addition <<
"-D" <<
id2string(pair.first) <<
"(";
866 std::vector<char> params(pair.second);
867 std::iota(params.begin(), params.end(),
'a');
868 for(std::vector<char>::iterator it=params.begin(); it!=params.end(); ++it)
871 if(it+1!=params.end())
875 new_argv.push_back(addition.str());
883 log.debug() <<
"RUN:";
884 for(std::size_t i=0; i<new_argv.size(); i++)
885 log.debug() <<
" " << new_argv[i];
894 bool have_files=
false;
896 for(goto_cc_cmdlinet::parsed_argvt::const_iterator
900 if(it->is_infile_name)
907 std::list<std::string> output_files;
918 for(goto_cc_cmdlinet::parsed_argvt::const_iterator
922 if(i_it->is_infile_name &&
933 output_files.push_back(
"a.out");
936 if(output_files.empty() ||
937 (output_files.size()==1 &&
938 output_files.front()==
"/dev/null"))
942 log.debug() <<
"Running " <<
native_tool_name <<
" to generate hybrid binary"
946 std::list<std::string> goto_binaries;
947 for(std::list<std::string>::const_iterator
948 it=output_files.begin();
949 it!=output_files.end();
964 goto_binaries.push_back(bin_name);
971 goto_binaries.size()==1 &&
972 output_files.size()==1)
975 output_files.front(),
976 goto_binaries.front(),
982 std::string native_tool;
991 for(std::list<std::string>::const_iterator
992 it=output_files.begin();
993 it!=output_files.end();
1012 const std::list<std::string> &preprocessed_source_files,
1016 bool have_files=
false;
1018 for(goto_cc_cmdlinet::parsed_argvt::const_iterator
1022 if(it->is_infile_name)
1042 std::map<std::string, std::string> output_files;
1047 for(
const auto &s : preprocessed_source_files)
1052 for(
const std::string &s : preprocessed_source_files)
1053 output_files.insert(
1057 if(output_files.empty() ||
1058 (output_files.size()==1 &&
1059 output_files.begin()->second==
"/dev/null"))
1062 log.debug() <<
"Appending preprocessed sources to generate hybrid asm output"
1065 for(
const auto &so : output_files)
1067 std::ifstream is(so.first);
1070 log.error() <<
"Failed to open input source " << so.first
1075 std::ofstream os(so.second, std::ios::app);
1078 log.error() <<
"Failed to open output file " << so.second
1083 const char comment=act_as_bcc ?
':' :
'#';
1089 while(std::getline(is, line))
1101 std::cout <<
"goto-cc understands the options of "
1102 <<
"gcc plus the following.\n\n";
Class that provides messages with a built-in verbosity 'level'.
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
@ COMPILE_LINK_EXECUTABLE
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
void set_arch_spec_arm(const irep_idt &subarch)
bool has_prefix(const std::string &s, const std::string &prefix)
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
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
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()
void help()
display command line help
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
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