39 const std::string &base_name)
41 if(cmdline.
isset(
"native-assembler"))
42 return cmdline.
get_value(
"native-assembler");
44 if(base_name==
"as86" ||
45 base_name.find(
"goto-as86")!=std::string::npos)
48 std::string::size_type
pos=base_name.find(
"goto-as");
50 if(
pos==std::string::npos)
53 std::string result=base_name;
54 result.replace(
pos, 7,
"as");
83 base_name.find(
"goto-as86")!=std::string::npos;
90 log.status() <<
"as86 version: 0.16.17 (goto-cc " <<
CBMC_VERSION <<
")"
95 log.status() <<
"GNU assembler version 2.20.51.0.7 20100318"
101 <<
"Copyright (C) 2006-2014 Daniel Kroening, Christoph Wintersteiger\n"
163 compiler.output_file_object=
"a.out";
164 compiler.output_file_executable=
"a.out";
171 for(goto_cc_cmdlinet::parsed_argvt::iterator
176 if(!
arg_it->is_infile_name)
199 while(std::getline(
is, line))
213 std::to_string(outputs)+
".i";
229 os << line.substr(2) <<
'\n';
239 log.warning() <<
"No GOTO-CC section found in " <<
arg_it->arg
277 for(std::size_t i=0; i<
new_argv.size(); i++)
309 catch(
const std::filesystem::filesystem_error &e)
333 std::cout <<
"goto-as understands the options of as plus the following.\n\n";
static std::string assembler_name(const cmdlinet &cmdline, const std::string &base_name)
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
int run_as()
run as or as86 with original command line
virtual void help_mode()
display command line help
virtual int doit()
does it.
as_modet(goto_cc_cmdlinet &_cmdline, const std::string &_base_name, bool _produce_hybrid_binary)
const bool produce_hybrid_binary
const std::string native_tool_name
int as_hybrid_binary(const compilet &compiler)
gcc_message_handlert message_handler
std::string get_value(char option) const
virtual bool isset(char option) const
@ COMPILE_LINK_EXECUTABLE
bool set(const cmdlinet &cmdline)
static irep_idt this_architecture()
static irep_idt this_operating_system()
struct configt::ansi_ct ansi_c
void print_warnings_as_errors(bool yes)
With yes set to true, prefix warnings with "error:" instead of "warning:".
goto_cc_cmdlinet & cmdline
const std::string base_name
void help()
display command line help
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.
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.
int run(const std::string &what, const std::vector< std::string > &argv)
#define PRECONDITION(CONDITION)
const char * CBMC_VERSION