44 const std::string &base_name)
46 if(cmdline.
isset(
"native-compiler"))
47 return cmdline.
get_value(
"native-compiler");
49 if(base_name==
"bcc" ||
50 base_name.find(
"goto-bcc")!=std::string::npos)
53 if(base_name==
"goto-clang")
56 std::string::size_type
pos=base_name.find(
"goto-gcc");
58 if(
pos==std::string::npos ||
59 base_name==
"goto-gcc" ||
69 std::string result=base_name;
70 result.replace(
pos, 8,
"gcc");
77 const std::string &base_name)
79 if(cmdline.
isset(
"native-linker"))
80 return cmdline.
get_value(
"native-linker");
82 std::string::size_type
pos=base_name.find(
"goto-ld");
84 if(
pos==std::string::npos ||
85 base_name==
"goto-gcc" ||
89 std::string result=base_name;
90 result.replace(
pos, 7,
"ld");
97 const std::string &_base_name,
98 bool _produce_hybrid_binary):
100 produce_hybrid_binary(_produce_hybrid_binary),
101 goto_binary_tmp_suffix(
".goto-cc-saved"),
121 "strongarm",
"strongarm110",
"strongarm1100",
"strongarm1110",
122 "arm2",
"arm250",
"arm3",
"arm6",
"arm60",
"arm600",
"arm610",
123 "arm620",
"fa526",
"fa626",
"fa606te",
"fa626te",
"fmp626",
124 "xscale",
"iwmmxt",
"iwmmxt2",
"xgene1"
127 "armv7",
"arm7m",
"arm7d",
"arm7dm",
"arm7di",
"arm7dmi",
128 "arm70",
"arm700",
"arm700i",
"arm710",
"arm710c",
"arm7100",
129 "arm720",
"arm7500",
"arm7500fe",
"arm7tdmi",
"arm7tdmi-s",
130 "arm710t",
"arm720t",
"arm740t",
"mpcore",
"mpcorenovfp",
131 "arm8",
"arm810",
"arm9",
"arm9e",
"arm920",
"arm920t",
132 "arm922t",
"arm946e-s",
"arm966e-s",
"arm968e-s",
"arm926ej-s",
133 "arm940t",
"arm9tdmi",
"arm10tdmi",
"arm1020t",
"arm1026ej-s",
134 "arm10e",
"arm1020e",
"arm1022e",
"arm1136j-s",
"arm1136jf-s",
135 "arm1156t2-s",
"arm1156t2f-s",
"arm1176jz-s",
"arm1176jzf-s",
136 "cortex-a5",
"cortex-a7",
"cortex-a8",
"cortex-a9",
137 "cortex-a12",
"cortex-a15",
"cortex-a53",
"cortex-r4",
138 "cortex-r4f",
"cortex-r5",
"cortex-r7",
"cortex-m7",
139 "cortex-m4",
"cortex-m3",
"cortex-m1",
"cortex-m0",
140 "cortex-m0plus",
"cortex-m1.small-multiply",
141 "cortex-m0.small-multiply",
"cortex-m0plus.small-multiply",
142 "marvell-pj4",
"ep9312",
"fa726te",
145 "cortex-a57",
"cortex-a72",
"exynos-m1"
147 {
"hppa", {
"1.0",
"1.1",
"2.0"}},
152 "powerpc",
"601",
"602",
"603",
"603e",
"604",
"604e",
"630",
156 "G4",
"7400",
"7450",
158 "401",
"403",
"405",
"405fp",
"440",
"440fp",
"464",
"464fp",
162 "e300c2",
"e300c3",
"e500mc",
"ec603e",
175 "power3",
"power4",
"power5",
"power5+",
"power6",
"power6x",
179 "e500mc64",
"e5500",
"e6500",
184 {
"powerpc64le", {
"powerpc64le",
"power8"}},
206 "loongson2e",
"loongson2f",
"loongson3a",
"mips64",
"mips64r2",
207 "mips64r3",
"mips64r5",
"mips64r6 4kc",
"5kc",
"5kf",
"20kc",
208 "octeon",
"octeon+",
"octeon2",
"octeon3",
"sb1",
"vr4100",
209 "vr4111",
"vr4120",
"vr4130",
"vr4300",
"vr5000",
"vr5400",
210 "vr5500",
"sr71000",
"xlp",
213 "mips32",
"mips32r2",
"mips32r3",
"mips32r5",
"mips32r6",
215 "4km",
"4kp",
"4ksc",
"4kec",
"4kem",
"4kep",
"4ksd",
"24kc",
216 "24kf2_1",
"24kf1_1",
"24kec",
"24kef2_1",
"24kef1_1",
"34kc",
217 "34kf2_1",
"34kf1_1",
"34kn",
"74kc",
"74kf2_1",
"74kf1_1",
218 "74kf3_2",
"1004kc",
"1004kf2_1",
"1004kf1_1",
"m4k",
"m14k",
219 "m14kc",
"m14ke",
"m14kec",
224 "mips1",
"mips2",
"r2000",
"r3000",
228 "mips3",
"mips4",
"r4000",
"r4400",
"r4600",
"r4650",
"r4700",
229 "r8000",
"rm7000",
"rm9000",
"r10000",
"r12000",
"r14000",
240 "z900",
"z990",
"g5",
"g6",
243 "z9-109",
"z9-ec",
"z10",
"z196",
"zEC12",
"z13"
251 "v7",
"v8",
"leon",
"leon3",
"leon3v7",
"cypress",
"supersparc",
252 "hypersparc",
"sparclite",
"f930",
"f934",
"sparclite86x",
256 "v9",
"ultrasparc",
"ultrasparc3",
"niagara",
"niagara2",
257 "niagara3",
"niagara4",
260 "itanium",
"itanium1",
"merced",
"itanium2",
"mckinley"
267 "i386",
"i486",
"i586",
"i686",
269 "k6",
"k6-2",
"k6-3",
"athlon" "athlon-tbird",
"athlon-4",
270 "athlon-xp",
"athlon-mp",
273 "pentium",
"pentium-mmx",
"pentiumpro" "pentium2",
"pentium3",
274 "pentium3m",
"pentium-m" "pentium4",
"pentium4m",
"prescott",
276 "winchip-c6",
"winchip2",
"c3",
"c3-2",
"geode",
280 "nocona",
"core2",
"nehalem" "westmere",
"sandybridge",
"knl",
281 "ivybridge",
"haswell",
"broadwell" "bonnell",
"silvermont",
283 "k8",
"k8-sse3",
"opteron",
"athlon64",
"athlon-fx",
284 "opteron-sse3" "athlon64-sse3",
"amdfam10",
"barcelona",
286 "bdver1",
"bdver2" "bdver3",
"bdver4",
328 base_name.find(
"goto-bcc")!=std::string::npos;
340 std::cout <<
"bcc: version " <<
gcc_version <<
" (goto-cc "
345 std::cout <<
"clang version " <<
gcc_version <<
" (goto-cc "
365 <<
"Copyright (C) 2006-2018 Daniel Kroening, Christoph Wintersteiger\n"
472 std::string target_cpu=
477 if(!target_cpu.empty())
481 for(
auto &processor : pair.second)
482 if(processor==target_cpu)
484 if(pair.first.find(
"mips")==std::string::npos)
492 if(pair.first==
"mips32o")
494 else if(pair.first==
"mips32n")
501 if(pair.first==
"mips32o")
503 else if(pair.first==
"mips32n")
531 switch(compiler.
mode)
546 log.debug() <<
"Compiling and linking a library" <<
messaget::eom;
549 log.debug() <<
"Compiling and linking an executable" <<
messaget::eom;
558 log.debug() <<
"Enabling Visual Studio syntax" <<
messaget::eom;
577 if(std_string==
"gnu89" || std_string==
"c89")
580 if(std_string==
"gnu99" || std_string==
"c99" || std_string==
"iso9899:1999" ||
581 std_string==
"gnu9x" || std_string==
"c9x" || std_string==
"iso9899:199x")
584 if(std_string==
"gnu11" || std_string==
"c11" ||
585 std_string==
"gnu1x" || std_string==
"c1x")
588 if(std_string==
"c++11" || std_string==
"c++1x" ||
589 std_string==
"gnu++11" || std_string==
"gnu++1x" ||
590 std_string==
"c++1y" ||
591 std_string==
"gnu++1y")
594 if(std_string==
"gnu++14" || std_string==
"c++14")
597 if(std_string ==
"gnu++17" || std_string ==
"c++17")
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);
709 else if(arg_it->arg==
"-x")
714 language=arg_it->arg;
721 language=std::string(arg_it->arg, 2, std::string::npos);
732 log.error() <<
"cannot specify -o with -c with multiple files"
761 const std::string &language,
762 const std::string &src,
763 const std::string &dest,
767 std::vector<std::string> new_argv;
771 bool skip_next=
false;
773 for(goto_cc_cmdlinet::parsed_argvt::const_iterator
783 else if(it->is_infile_name)
787 else if(it->arg==
"-c" || it->arg==
"-E" || it->arg==
"-S")
791 else if(it->arg==
"-o")
800 new_argv.push_back(it->arg);
804 new_argv.push_back(
"-E");
807 std::string stdout_file;
812 new_argv.push_back(
"-o");
813 new_argv.push_back(dest);
817 if(!language.empty())
819 new_argv.push_back(
"-x");
820 new_argv.push_back(language);
824 new_argv.push_back(src);
827 INVARIANT(new_argv.size()>=1,
"No program name in argv");
831 log.debug() <<
"RUN:";
832 for(std::size_t i=0; i<new_argv.size(); i++)
833 log.debug() <<
" " << new_argv[i];
844 std::vector<std::string> new_argv;
847 new_argv.push_back(a.arg);
852 std::map<irep_idt, std::size_t> arities;
854 for(
const auto &pair : arities)
856 std::ostringstream addition;
857 addition <<
"-D" <<
id2string(pair.first) <<
"(";
858 std::vector<char> params(pair.second);
859 std::iota(params.begin(), params.end(),
'a');
860 for(std::vector<char>::iterator it=params.begin(); it!=params.end(); ++it)
863 if(it+1!=params.end())
867 new_argv.push_back(addition.str());
875 log.debug() <<
"RUN:";
876 for(std::size_t i=0; i<new_argv.size(); i++)
877 log.debug() <<
" " << new_argv[i];
886 bool have_files=
false;
888 for(goto_cc_cmdlinet::parsed_argvt::const_iterator
892 if(it->is_infile_name)
899 std::list<std::string> output_files;
910 for(goto_cc_cmdlinet::parsed_argvt::const_iterator
914 if(i_it->is_infile_name &&
925 output_files.push_back(
"a.out");
928 if(output_files.empty() ||
929 (output_files.size()==1 &&
930 output_files.front()==
"/dev/null"))
934 log.debug() <<
"Running " <<
native_tool_name <<
" to generate hybrid binary"
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();
956 goto_binaries.push_back(bin_name);
963 goto_binaries.size()==1 &&
964 output_files.size()==1)
967 output_files.front(),
968 goto_binaries.front(),
974 std::string native_tool;
983 for(std::list<std::string>::const_iterator
984 it=output_files.begin();
985 it!=output_files.end();
1004 const std::list<std::string> &preprocessed_source_files,
1008 bool have_files=
false;
1010 for(goto_cc_cmdlinet::parsed_argvt::const_iterator
1014 if(it->is_infile_name)
1034 std::map<std::string, std::string> output_files;
1039 for(
const auto &s : preprocessed_source_files)
1044 for(
const std::string &s : preprocessed_source_files)
1045 output_files.insert(
1049 if(output_files.empty() ||
1050 (output_files.size()==1 &&
1051 output_files.begin()->second==
"/dev/null"))
1054 log.debug() <<
"Appending preprocessed sources to generate hybrid asm output"
1057 for(
const auto &so : output_files)
1059 std::ifstream is(so.first);
1062 log.error() <<
"Failed to open input source " << so.first
1067 std::ofstream os(so.second, std::ios::app);
1070 log.error() <<
"Failed to open output file " << so.second
1075 const char comment=act_as_bcc ?
':' :
'#';
1081 while(std::getline(is, line))
1093 std::cout <<
"goto-cc understands the options of "
1094 <<
"gcc plus the following.\n\n";
std::string get_value(char option) const
virtual bool isset(char option) const
const std::list< std::string > & get_values(const std::string &option) const
@ COMPILE_LINK_EXECUTABLE
std::string output_file_object
bool add_input_file(const std::string &)
puts input file names into a list and does preprocessing for libraries.
std::list< std::string > libraries
void cprover_macro_arities(std::map< irep_idt, std::size_t > &cprover_macros) const
__CPROVER_... macros written to object files and their arities
std::list< std::string > object_files
bool doit()
reads and source and object files, compiles and links them into goto program objects.
std::list< std::string > source_files
bool wrote_object_files() const
Has this compiler written any object files?
std::string object_file_extension
std::list< std::string > library_paths
std::string output_file_executable
void set_arch(const irep_idt &)
bool set(const cmdlinet &cmdline)
static irep_idt this_architecture()
static irep_idt this_operating_system()
struct configt::ansi_ct ansi_c
Base class for exceptions thrown in the cprover project.
virtual std::string what() const =0
A human readable description of what went wrong.
std::string native_tool_name
int preprocess(const std::string &language, const std::string &src, const std::string &dest, bool act_as_bcc)
call gcc for preprocessing
gcc_modet(goto_cc_cmdlinet &_cmdline, const std::string &_base_name, bool _produce_hybrid_binary)
static bool needs_preprocessing(const std::string &)
const std::string goto_binary_tmp_suffix
int run_gcc(const compilet &compiler)
call gcc with original command line
gcc_message_handlert gcc_message_handler
void help_mode() final
display command line help
const std::map< std::string, std::set< std::string > > arch_map
Associate CBMC architectures with processor names.
const bool produce_hybrid_binary
int asm_output(bool act_as_bcc, const std::list< std::string > &preprocessed_source_files, const compilet &compiler)
int gcc_hybrid_binary(compilet &compiler)
void get(const std::string &executable)
configt::cppt::cpp_standardt default_cxx_standard
configt::ansi_ct::c_standardt default_c_standard
enum gcc_versiont::flavort flavor
bool have_infile_arg() const
goto_cc_cmdlinet & cmdline
const std::string base_name
void help()
display command line help
Synthesise definitions of symbols that are defined in linker scripts.
int add_linker_script_definitions()
Add values of linkerscript-defined symbols to the goto-binary.
Class that provides messages with a built-in verbosity 'level'.
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.
Compile and link source and object files.
bool has_prefix(const std::string &s, const std::string &prefix)
void file_rename(const std::string &old_path, const std::string &new_path)
Rename a file.
static std::string linker_name(const cmdlinet &cmdline, const std::string &base_name)
static std::string compiler_name(const cmdlinet &cmdline, const std::string &base_name)
Base class for command line interpretation.
void configure_gcc(const gcc_versiont &gcc_version)
std::string get_base_name(const std::string &in, bool strip_suffix)
cleans a filename from path and extension
Command line interpretation for goto-cc.
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, bool linking_efi)
Merges a goto binary into an object file (e.g.
Create hybrid binary with goto-binary section.
const std::string & id2string(const irep_idt &d)
Merge linker script-defined symbols into a goto-program.
static std::string comment(const rw_set_baset::entryt &entry, bool write)
int run(const std::string &what, const std::vector< std::string > &argv)
#define PRECONDITION(CONDITION)
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
enum configt::ansi_ct::c_standardt c_standard
std::list< std::string > undefines
std::list< std::string > preprocessor_options
bool single_precision_constant
void set_arch_spec_arm(const irep_idt &subarch)
std::size_t wchar_t_width
void set_arch_spec_x86_64()
void set_arch_spec_i386()
std::size_t short_int_width
enum configt::cppt::cpp_standardt cpp_standard
bool has_suffix(const std::string &s, const std::string &suffix)
const char * CBMC_VERSION