17 #define EX_SOFTWARE 70 54 const std::string &base_name)
56 if(cmdline.
isset(
"native-compiler"))
57 return cmdline.
get_value(
"native-compiler");
59 if(base_name==
"bcc" ||
60 base_name.find(
"goto-bcc")!=std::string::npos)
65 if(
pos==std::string::npos ||
66 base_name==
"goto-gcc" ||
76 std::string result=base_name;
77 result.replace(
pos, 8,
"gcc");
84 const std::string &base_name)
86 if(cmdline.
isset(
"native-linker"))
87 return cmdline.
get_value(
"native-linker");
91 if(
pos==std::string::npos ||
92 base_name==
"goto-gcc" ||
96 std::string result=base_name;
97 result.replace(
pos, 7,
"ld");
104 const std::string &_base_name,
105 bool _produce_hybrid_binary):
107 produce_hybrid_binary(_produce_hybrid_binary),
108 goto_binary_tmp_suffix(
".goto-cc-saved"),
128 "strongarm",
"strongarm110",
"strongarm1100",
"strongarm1110",
129 "arm2",
"arm250",
"arm3",
"arm6",
"arm60",
"arm600",
"arm610",
130 "arm620",
"fa526",
"fa626",
"fa606te",
"fa626te",
"fmp626",
131 "xscale",
"iwmmxt",
"iwmmxt2",
"xgene1" 134 "armv7",
"arm7m",
"arm7d",
"arm7dm",
"arm7di",
"arm7dmi",
135 "arm70",
"arm700",
"arm700i",
"arm710",
"arm710c",
"arm7100",
136 "arm720",
"arm7500",
"arm7500fe",
"arm7tdmi",
"arm7tdmi-s",
137 "arm710t",
"arm720t",
"arm740t",
"mpcore",
"mpcorenovfp",
138 "arm8",
"arm810",
"arm9",
"arm9e",
"arm920",
"arm920t",
139 "arm922t",
"arm946e-s",
"arm966e-s",
"arm968e-s",
"arm926ej-s",
140 "arm940t",
"arm9tdmi",
"arm10tdmi",
"arm1020t",
"arm1026ej-s",
141 "arm10e",
"arm1020e",
"arm1022e",
"arm1136j-s",
"arm1136jf-s",
142 "arm1156t2-s",
"arm1156t2f-s",
"arm1176jz-s",
"arm1176jzf-s",
143 "cortex-a5",
"cortex-a7",
"cortex-a8",
"cortex-a9",
144 "cortex-a12",
"cortex-a15",
"cortex-a53",
"cortex-r4",
145 "cortex-r4f",
"cortex-r5",
"cortex-r7",
"cortex-m7",
146 "cortex-m4",
"cortex-m3",
"cortex-m1",
"cortex-m0",
147 "cortex-m0plus",
"cortex-m1.small-multiply",
148 "cortex-m0.small-multiply",
"cortex-m0plus.small-multiply",
149 "marvell-pj4",
"ep9312",
"fa726te",
152 "cortex-a57",
"cortex-a72",
"exynos-m1" 154 {
"hppa", {
"1.0",
"1.1",
"2.0"}},
159 "powerpc",
"601",
"602",
"603",
"603e",
"604",
"604e",
"630",
163 "G4",
"7400",
"7450",
165 "401",
"403",
"405",
"405fp",
"440",
"440fp",
"464",
"464fp",
169 "e300c2",
"e300c3",
"e500mc",
"ec603e",
182 "power3",
"power4",
"power5",
"power5+",
"power6",
"power6x",
186 "e500mc64",
"e5500",
"e6500",
191 {
"powerpc64le", {
"powerpc64le",
"power8"}},
213 "loongson2e",
"loongson2f",
"loongson3a",
"mips64",
"mips64r2",
214 "mips64r3",
"mips64r5",
"mips64r6 4kc",
"5kc",
"5kf",
"20kc",
215 "octeon",
"octeon+",
"octeon2",
"octeon3",
"sb1",
"vr4100",
216 "vr4111",
"vr4120",
"vr4130",
"vr4300",
"vr5000",
"vr5400",
217 "vr5500",
"sr71000",
"xlp",
220 "mips32",
"mips32r2",
"mips32r3",
"mips32r5",
"mips32r6",
222 "4km",
"4kp",
"4ksc",
"4kec",
"4kem",
"4kep",
"4ksd",
"24kc",
223 "24kf2_1",
"24kf1_1",
"24kec",
"24kef2_1",
"24kef1_1",
"34kc",
224 "34kf2_1",
"34kf1_1",
"34kn",
"74kc",
"74kf2_1",
"74kf1_1",
225 "74kf3_2",
"1004kc",
"1004kf2_1",
"1004kf1_1",
"m4k",
"m14k",
226 "m14kc",
"m14ke",
"m14kec",
231 "mips1",
"mips2",
"r2000",
"r3000",
235 "mips3",
"mips4",
"r4000",
"r4400",
"r4600",
"r4650",
"r4700",
236 "r8000",
"rm7000",
"rm9000",
"r10000",
"r12000",
"r14000",
247 "z900",
"z990",
"g5",
"g6",
250 "z9-109",
"z9-ec",
"z10",
"z196",
"zEC12",
"z13" 258 "v7",
"v8",
"leon",
"leon3",
"leon3v7",
"cypress",
"supersparc",
259 "hypersparc",
"sparclite",
"f930",
"f934",
"sparclite86x",
263 "v9",
"ultrasparc",
"ultrasparc3",
"niagara",
"niagara2",
264 "niagara3",
"niagara4",
267 "itanium",
"itanium1",
"merced",
"itanium2",
"mckinley" 274 "i386",
"i486",
"i586",
"i686",
276 "k6",
"k6-2",
"k6-3",
"athlon" "athlon-tbird",
"athlon-4",
277 "athlon-xp",
"athlon-mp",
280 "pentium",
"pentium-mmx",
"pentiumpro" "pentium2",
"pentium3",
281 "pentium3m",
"pentium-m" "pentium4",
"pentium4m",
"prescott",
283 "winchip-c6",
"winchip2",
"c3",
"c3-2",
"geode",
287 "nocona",
"core2",
"nehalem" "westmere",
"sandybridge",
"knl",
288 "ivybridge",
"haswell",
"broadwell" "bonnell",
"silvermont",
290 "k8",
"k8-sse3",
"opteron",
"athlon64",
"athlon-fx",
291 "opteron-sse3" "athlon64-sse3",
"amdfam10",
"barcelona",
293 "bdver1",
"bdver2" "bdver3",
"bdver4",
335 base_name.find(
"goto-bcc")!=std::string::npos;
348 <<
" (goto-cc " CBMC_VERSION
")\n";
353 <<
" (goto-cc " CBMC_VERSION
")\n";
355 std::cout <<
"gcc (goto-cc " CBMC_VERSION
") " <<
gcc_version <<
'\n';
372 <<
"Copyright (C) 2006-2018 Daniel Kroening, Christoph Wintersteiger\n" 373 <<
"CBMC version: " CBMC_VERSION <<
'\n' 409 debug() <<
"BCC mode (hybrid)" <<
eom;
416 debug() <<
"GCC mode (hybrid)" <<
eom;
474 std::string target_cpu=
483 for(
auto &processor : pair.second)
484 if(processor==target_cpu)
486 if(pair.first.find(
"mips")==std::string::npos)
494 if(pair.first==
"mips32o")
496 else if(pair.first==
"mips32n")
503 if(pair.first==
"mips32o")
505 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;
570 compiler.object_file_extension=
"s";
572 compiler.object_file_extension=
"o";
578 if(std_string==
"gnu89" || std_string==
"c89")
581 if(std_string==
"gnu99" || std_string==
"c99" || std_string==
"iso9899:1999" ||
582 std_string==
"gnu9x" || std_string==
"c9x" || std_string==
"iso9899:199x")
585 if(std_string==
"gnu11" || std_string==
"c11" ||
586 std_string==
"gnu1x" || std_string==
"c1x")
589 if(std_string==
"c++11" || std_string==
"c++1x" ||
590 std_string==
"gnu++11" || std_string==
"gnu++1x" ||
591 std_string==
"c++1y" ||
592 std_string==
"gnu++1y")
595 if(std_string==
"gnu++14" || std_string==
"c++14")
636 compiler.libraries.push_back(
"c");
639 compiler.libraries.push_back(
"pthread");
650 compiler.output_file_object=
"";
651 compiler.output_file_executable=
"a.out";
659 std::string language;
661 for(goto_cc_cmdlinet::parsed_argvt::iterator
666 if(arg_it->is_infile_name)
670 if(language==
"cpp-output" || language==
"c++-cpp-output")
672 compiler.add_input_file(arg_it->arg);
674 else if(language==
"c" || language==
"c++" ||
677 std::string new_suffix;
681 else if(language==
"c++")
684 new_suffix=
has_suffix(arg_it->arg,
".c")?
".i":
".ii";
686 std::string new_name=
688 std::string dest=temp_dir(new_name);
691 preprocess(language, arg_it->arg, dest, act_as_bcc);
695 error() <<
"preprocessing has failed" <<
eom;
699 compiler.add_input_file(dest);
702 compiler.add_input_file(arg_it->arg);
704 else if(arg_it->arg==
"-x")
709 language=arg_it->arg;
716 language=std::string(arg_it->arg, 2, std::string::npos);
726 if(compiler.source_files.empty() &&
727 compiler.object_files.empty())
731 return asm_output(act_as_bcc, compiler.source_files, compiler);
747 const std::string &language,
748 const std::string &src,
749 const std::string &dest,
753 std::vector<std::string> new_argv;
757 bool skip_next=
false;
759 for(goto_cc_cmdlinet::parsed_argvt::const_iterator
769 else if(it->is_infile_name)
773 else if(it->arg==
"-c" || it->arg==
"-E" || it->arg==
"-S")
777 else if(it->arg==
"-o")
786 new_argv.push_back(it->arg);
790 new_argv.push_back(
"-E");
793 std::string stdout_file;
798 new_argv.push_back(
"-o");
799 new_argv.push_back(dest);
805 new_argv.push_back(
"-x");
806 new_argv.push_back(language);
810 new_argv.push_back(src);
813 INVARIANT(new_argv.size()>=1,
"No program name in argv");
817 for(std::size_t i=0; i<new_argv.size(); i++)
818 debug() <<
" " << new_argv[i];
829 std::vector<std::string> new_argv;
832 new_argv.push_back(a.arg);
837 std::map<irep_idt, std::size_t> arities;
839 for(
const auto &pair : arities)
841 std::ostringstream addition;
842 addition <<
"-D" <<
id2string(pair.first) <<
"(";
843 std::vector<char> params(pair.second);
844 std::iota(params.begin(), params.end(),
'a');
845 for(std::vector<char>::iterator it=params.begin(); it!=params.end(); ++it)
848 if(it+1!=params.end())
852 new_argv.push_back(addition.str());
860 for(std::size_t i=0; i<new_argv.size(); i++)
861 debug() <<
" " << new_argv[i];
870 bool have_files=
false;
872 for(goto_cc_cmdlinet::parsed_argvt::const_iterator
876 if(it->is_infile_name)
883 std::list<std::string> output_files;
894 for(goto_cc_cmdlinet::parsed_argvt::const_iterator
898 if(i_it->is_infile_name &&
909 output_files.push_back(
"a.out");
912 if(output_files.empty() ||
913 (output_files.size()==1 &&
914 output_files.front()==
"/dev/null"))
918 <<
" to generate hybrid binary" <<
eom;
921 std::list<std::string> goto_binaries;
922 for(std::list<std::string>::const_iterator
923 it=output_files.begin();
924 it!=output_files.end();
928 int result=rename(it->c_str(), bin_name.c_str());
931 error() <<
"Rename failed: " << std::strerror(errno) <<
eom;
934 goto_binaries.push_back(bin_name);
941 goto_binaries.size()==1 &&
942 output_files.size()==1)
945 compiler, output_files.front(), goto_binaries.front(),
947 result=ls_merge.add_linker_script_definitions();
950 std::string native_tool;
959 for(std::list<std::string>::const_iterator
960 it=output_files.begin();
961 it!=output_files.end();
976 const std::list<std::string> &preprocessed_source_files,
980 bool have_files=
false;
982 for(goto_cc_cmdlinet::parsed_argvt::const_iterator
986 if(it->is_infile_name)
996 <<
" to generate native asm output" <<
eom;
1004 std::map<std::string, std::string> output_files;
1009 for(
const auto &s : preprocessed_source_files)
1014 for(
const std::string &s : preprocessed_source_files)
1015 output_files.insert(
1019 if(output_files.empty() ||
1020 (output_files.size()==1 &&
1021 output_files.begin()->second==
"/dev/null"))
1025 <<
"Appending preprocessed sources to generate hybrid asm output" 1028 for(
const auto &so : output_files)
1030 std::ifstream is(so.first);
1033 error() <<
"Failed to open input source " << so.first <<
eom;
1037 std::ofstream os(so.second, std::ios::app);
1040 error() <<
"Failed to open output file " << so.second <<
eom;
1044 const char comment=act_as_bcc ?
':' :
'#';
1050 while(std::getline(is, line))
1062 std::cout <<
"goto-cc understands the options of " 1063 <<
"gcc plus the following.\n\n";
void set_arch_spec_arm(const irep_idt &subarch)
const bool produce_hybrid_binary
const std::list< std::string > & get_values(const std::string &option) const
struct configt::ansi_ct ansi_c
const std::string & id2string(const irep_idt &d)
enum gcc_versiont::flavort flavor
const std::string goto_binary_tmp_suffix
int run_gcc(const compilet &compiler)
call gcc with original command line
std::string comment(const rw_set_baset::entryt &entry, bool write)
int asm_output(bool act_as_bcc, const std::list< std::string > &preprocessed_source_files, const compilet &compiler)
bool single_precision_constant
int run(const std::string &what, const std::vector< std::string > &argv, const std::string &std_input, const std::string &std_output, const std::string &std_error)
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...
std::string get_value(char option) const
Base class for command line interpretation.
unsignedbv_typet size_type()
std::list< std::string > undefines
bool wrote_object_files() const
Has this compiler written any object files?
static mstreamt & eom(mstreamt &m)
std::string get_base_name(const std::string &in, bool strip_suffix)
cleans a filename from path and extension
gcc_message_handlert gcc_message_handler
void get(const std::string &executable)
#define INVARIANT(CONDITION, REASON)
void cprover_macro_arities(std::map< irep_idt, std::size_t > &cprover_macros) const
__CPROVER_... macros written to object files and their arities
static std::string linker_name(const cmdlinet &cmdline, const std::string &base_name)
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)
virtual bool isset(char option) const
Create hybrid binary with goto-binary section.
void set_arch_spec_x86_64()
gcc_modet(goto_cc_cmdlinet &_cmdline, const std::string &_base_name, bool _produce_hybrid_binary)
void set_arch(const irep_idt &)
goto_cc_cmdlinet & cmdline
bool is_at_least(unsigned v_major, unsigned v_minor=0, unsigned v_patchlevel=0) const
enum configt::cppt::cpp_standardt cpp_standard
#define PRECONDITION(CONDITION)
bool has_prefix(const std::string &s, const std::string &prefix)
configt::ansi_ct::c_standardt default_c_standard
void help_mode() final
display command line help
enum configt::ansi_ct::c_standardt c_standard
std::size_t wchar_t_width
int gcc_hybrid_binary(compilet &compiler)
static bool needs_preprocessing(const std::string &)
static irep_idt this_operating_system()
message_handlert & get_message_handler()
mstreamt & result() const
std::string native_tool_name
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.
virtual void help()
display command line help
void set_arch_spec_i386()
bool have_infile_arg() const
const std::map< std::string, std::set< std::string > > arch_map
Associate CBMC architectures with processor names.
static std::string compiler_name(const cmdlinet &cmdline, const std::string &base_name)
bool has_suffix(const std::string &s, const std::string &suffix)
Merge linker script-defined symbols into a goto-program.
std::list< std::string > preprocessor_options
configt::cppt::cpp_standardt default_cxx_standard
bool ts_18661_3_Floatn_types
const std::string base_name
static irep_idt this_architecture()
std::size_t short_int_width
Synthesise definitions of symbols that are defined in linker scripts.