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",
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"
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")
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;
628 config.
ansi_c.preprocessor_options.push_back(
"-nostdinc");
641 compiler.libraries.push_back(
"pthread");
653 compiler.output_file_executable=
"a.out";
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++" ||
684 else if(language==
"c++")
692 temp_dirs.emplace_back(
"goto-cc-XXXXXX");
709 else if(
arg_it->arg==
"-x")
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,
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")
817 if(!language.empty())
831 log.debug() <<
"RUN:";
852 std::map<irep_idt, std::size_t>
arities;
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())
875 log.debug() <<
"RUN:";
888 for(goto_cc_cmdlinet::parsed_argvt::const_iterator
892 if(it->is_infile_name)
910 for(goto_cc_cmdlinet::parsed_argvt::const_iterator
914 if(
i_it->is_infile_name &&
934 log.debug() <<
"Running " <<
native_tool_name <<
" to generate hybrid binary"
939 for(std::list<std::string>::const_iterator
971 result=
ls_merge.add_linker_script_definitions();
983 for(std::list<std::string>::const_iterator
1010 for(goto_cc_cmdlinet::parsed_argvt::const_iterator
1014 if(it->is_infile_name)
1054 log.debug() <<
"Appending preprocessed sources to generate hybrid asm output"
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
1081 while(std::getline(
is, line))
1093 std::cout <<
"goto-cc understands the options of "
1094 <<
"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 =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.
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