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");
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",
321 base_name.find(
"goto-bcc")!=std::string::npos;
333 std::cout <<
"bcc: version " <<
gcc_version <<
" (goto-cc "
338 std::cout <<
"clang version " <<
gcc_version <<
" (goto-cc "
358 <<
"Copyright (C) 2006-2018 Daniel Kroening, Christoph Wintersteiger\n"
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")
523 static const std::map<std::string, std::string> target_map = {
524 {
"aarch64",
"arm64" },
525 {
"aarch64_32",
"arm" },
526 {
"aarch64_be",
"none" },
530 {
"arm64_32",
"arm" },
536 {
"hexagon",
"none" },
540 {
"mips64",
"mips64" },
541 {
"mips64el",
"mips64el" },
542 {
"mipsel",
"mipsel" },
545 {
"nvptx64",
"none" },
546 {
"ppc32",
"powerpc" },
548 {
"ppc64le",
"ppc64le" },
550 {
"riscv32",
"none" },
551 {
"riscv64",
"riscv64" },
553 {
"sparcel",
"none" },
554 {
"sparcv9",
"sparc64" },
555 {
"systemz",
"none" },
557 {
"thumbeb",
"none" },
561 {
"x86_64",
"x86_64" },
567 if(it == target_map.end())
607 log.debug() <<
"Compiling and linking a library" <<
messaget::eom;
610 log.debug() <<
"Compiling and linking an executable" <<
messaget::eom;
619 log.debug() <<
"Enabling Visual Studio syntax" <<
messaget::eom;
689 config.
ansi_c.preprocessor_options.push_back(
"-nostdinc");
702 compiler.libraries.push_back(
"pthread");
714 compiler.output_file_executable=
"a.out";
722 std::string language;
724 for(goto_cc_cmdlinet::parsed_argvt::iterator
729 if(
arg_it->is_infile_name)
733 if(language==
"cpp-output" || language==
"c++-cpp-output")
738 language ==
"c" || language ==
"c++" ||
745 else if(language==
"c++")
753 temp_dirs.emplace_back(
"goto-cc-XXXXXX");
770 else if(
arg_it->arg==
"-x")
782 language=std::string(
arg_it->arg, 2, std::string::npos);
793 log.error() <<
"cannot specify -o with -c with multiple files"
822 const std::string &language,
823 const std::string &src,
824 const std::string &dest,
834 for(goto_cc_cmdlinet::parsed_argvt::const_iterator
844 else if(it->is_infile_name)
848 else if(it->arg==
"-c" || it->arg==
"-E" || it->arg==
"-S")
852 else if(it->arg==
"-o")
878 if(!language.empty())
892 log.debug() <<
"RUN:";
893 for(std::size_t i=0; i<
new_argv.size(); i++)
913 std::map<irep_idt, std::size_t>
arities;
919 std::vector<char> params(
pair.second);
920 std::iota(params.begin(), params.end(),
'a');
921 for(std::vector<char>::iterator it=params.begin(); it!=params.end(); ++it)
924 if(it+1!=params.end())
936 log.debug() <<
"RUN:";
937 for(std::size_t i=0; i<
new_argv.size(); i++)
949 for(goto_cc_cmdlinet::parsed_argvt::const_iterator
953 if(it->is_infile_name)
971 for(goto_cc_cmdlinet::parsed_argvt::const_iterator
975 if(
i_it->is_infile_name &&
995 log.debug() <<
"Running " <<
native_tool_name <<
" to generate hybrid binary"
1000 for(std::list<std::string>::const_iterator
1032 result=
ls_merge.add_linker_script_definitions();
1044 for(std::list<std::string>::const_iterator
1071 for(goto_cc_cmdlinet::parsed_argvt::const_iterator
1075 if(it->is_infile_name)
1115 log.debug() <<
"Appending preprocessed sources to generate hybrid asm output"
1120 std::ifstream
is(
so.first);
1123 log.error() <<
"Failed to open input source " <<
so.first
1128 std::ofstream os(
so.second, std::ios::app);
1131 log.error() <<
"Failed to open output file " <<
so.second
1142 while(std::getline(
is, line))
1154 std::cout <<
"goto-cc understands the options of "
1155 <<
"gcc plus the following.\n\n";
virtual void clear()
Reset the abstract state.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
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
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
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.
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'.
bool has_suffix(const std::string &s, const std::string &suffix)
const char * CBMC_VERSION