Go to the documentation of this file.
17 #define EX_SOFTWARE 70
38 const std::string &base_name)
40 if(cmdline.
isset(
"native-assembler"))
41 return cmdline.
get_value(
"native-assembler");
43 if(base_name==
"as86" ||
44 base_name.find(
"goto-as86")!=std::string::npos)
49 if(
pos==std::string::npos)
52 std::string result=base_name;
53 result.replace(
pos, 7,
"as");
60 const std::string &_base_name,
61 bool _produce_hybrid_binary):
63 produce_hybrid_binary(_produce_hybrid_binary),
80 base_name.find(
"goto-as86")!=std::string::npos;
89 status() <<
"GNU assembler version 2.20.51.0.7 20100318"
94 <<
"Copyright (C) 2006-2014 Daniel Kroening, Christoph Wintersteiger\n"
110 debug() <<
"AS86 mode (hybrid)" <<
eom;
117 debug() <<
"AS mode (hybrid)" <<
eom;
131 debug() <<
"Compiling and linking an executable" <<
eom;
136 debug() <<
"Compiling and linking a library" <<
eom;
163 for(goto_cc_cmdlinet::parsed_argvt::iterator
168 if(!arg_it->is_infile_name)
173 std::ifstream is(infile);
176 error() <<
"Failed to open input source " << infile <<
eom;
187 const std::string comment2=act_as_as86 ?
"::" :
"##";
191 while(std::getline(is, line))
193 if(line==comment2+
" GOTO-CC")
197 assert(!dest.empty());
203 std::string new_name=
206 dest=temp_dir(new_name);
211 error() <<
"Failed to tmp output file " << dest <<
eom;
221 os << line.substr(2) <<
'\n';
226 assert(!dest.empty());
230 warning() <<
"No GOTO-CC section found in " << arg_it->arg <<
eom;
256 std::vector<std::string> new_argv;
259 new_argv.push_back(a.arg);
266 for(std::size_t i=0; i<new_argv.size(); i++)
267 std::cout <<
" " << new_argv[i];
276 std::string output_file=
"a.out";
285 if(output_file==
"/dev/null")
289 <<
" to generate hybrid binary" <<
eom;
292 std::string saved = output_file +
".goto-cc-saved";
321 std::cout <<
"goto-as understands the options of as plus the following.\n\n";
std::string get_base_name(const std::string &in, bool strip_suffix)
cleans a filename from path and extension
const std::string native_tool_name
virtual bool isset(char option) const
std::list< std::string > source_files
mstreamt & status() const
bool doit()
reads and source and object files, compiles and links them into goto program objects.
int run(const std::string &what, const std::vector< std::string > &argv)
const std::string base_name
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
struct configt::ansi_ct ansi_c
int run_as()
run as or as86 with original command line
int as_hybrid_binary(const compilet &compiler)
const char * CBMC_VERSION
std::string output_file_object
mstreamt & result() const
std::string output_file_executable
virtual std::string what() const =0
A human readable description of what went wrong.
std::string get_value(char option) const
Compile and link source and object files.
as_modet(goto_cc_cmdlinet &_cmdline, const std::string &_base_name, bool _produce_hybrid_binary)
static irep_idt this_operating_system()
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)
Merges a goto binary into an object file (e.g.
std::string object_file_extension
goto_cc_cmdlinet & cmdline
@ COMPILE_LINK_EXECUTABLE
gcc_message_handlert message_handler
bool add_input_file(const std::string &)
puts input file names into a list and does preprocessing for libraries.
const bool produce_hybrid_binary
Create hybrid binary with goto-binary section.
static irep_idt this_architecture()
message_handlert & get_message_handler()
bool set(const cmdlinet &cmdline)
static std::string assembler_name(const cmdlinet &cmdline, const std::string &base_name)
virtual void help_mode()
display command line help
void help()
display command line help
unsignedbv_typet size_type()
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.
mstreamt & warning() const
virtual int doit()
does it.
Base class for exceptions thrown in the cprover project.
void file_rename(const std::string &old_path, const std::string &new_path)
Rename a file.