17 #define EX_SOFTWARE 70
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)
50 if(
pos==std::string::npos)
53 std::string result=base_name;
54 result.replace(
pos, 7,
"as");
61 const std::string &_base_name,
62 bool _produce_hybrid_binary):
64 produce_hybrid_binary(_produce_hybrid_binary),
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"
171 for(goto_cc_cmdlinet::parsed_argvt::iterator
176 if(!arg_it->is_infile_name)
181 std::ifstream is(infile);
195 const std::string comment2=act_as_as86 ?
"::" :
"##";
199 while(std::getline(is, line))
201 if(line==comment2+
" GOTO-CC")
211 std::string new_name=
214 dest=temp_dir(new_name);
229 os << line.substr(2) <<
'\n';
239 log.warning() <<
"No GOTO-CC section found in " << arg_it->arg
267 std::vector<std::string> new_argv;
270 new_argv.push_back(a.arg);
277 for(std::size_t i=0; i<new_argv.size(); i++)
278 std::cout <<
" " << new_argv[i];
287 std::string output_file=
"a.out";
296 if(output_file==
"/dev/null")
304 std::string saved = output_file +
".goto-cc-saved";
307 std::filesystem::rename(output_file, saved);
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)
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
std::string output_file_object
bool add_input_file(const std::string &)
puts input file names into a list and does preprocessing for libraries.
bool doit()
reads and source and object files, compiles and links them into goto program objects.
std::list< std::string > source_files
std::string object_file_extension
std::string output_file_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)
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
const char * CBMC_VERSION