Go to the documentation of this file.
17 #define EX_SOFTWARE 70
37 const std::string &base_name)
39 if(cmdline.
isset(
"native-assembler"))
40 return cmdline.
get_value(
"native-assembler");
42 if(base_name==
"as86" ||
43 base_name.find(
"goto-as86")!=std::string::npos)
48 if(
pos==std::string::npos)
51 std::string result=base_name;
52 result.replace(
pos, 7,
"as");
59 const std::string &_base_name,
60 bool _produce_hybrid_binary):
62 produce_hybrid_binary(_produce_hybrid_binary),
79 base_name.find(
"goto-as86")!=std::string::npos;
88 status() <<
"GNU assembler version 2.20.51.0.7 20100318"
93 <<
"Copyright (C) 2006-2014 Daniel Kroening, Christoph Wintersteiger\n"
109 debug() <<
"AS86 mode (hybrid)" <<
eom;
116 debug() <<
"AS mode (hybrid)" <<
eom;
130 debug() <<
"Compiling and linking an executable" <<
eom;
135 debug() <<
"Compiling and linking a library" <<
eom;
162 for(goto_cc_cmdlinet::parsed_argvt::iterator
167 if(!arg_it->is_infile_name)
172 std::ifstream is(infile);
175 error() <<
"Failed to open input source " << infile <<
eom;
186 const std::string comment2=act_as_as86 ?
"::" :
"##";
190 while(std::getline(is, line))
192 if(line==comment2+
" GOTO-CC")
196 assert(!dest.empty());
202 std::string new_name=
205 dest=temp_dir(new_name);
210 error() <<
"Failed to tmp output file " << dest <<
eom;
220 os << line.substr(2) <<
'\n';
225 assert(!dest.empty());
229 warning() <<
"No GOTO-CC section found in " << arg_it->arg <<
eom;
255 std::vector<std::string> new_argv;
258 new_argv.push_back(a.arg);
265 for(std::size_t i=0; i<new_argv.size(); i++)
266 std::cout <<
" " << new_argv[i];
275 std::string output_file=
"a.out";
284 if(output_file==
"/dev/null")
288 <<
" to generate hybrid binary" <<
eom;
293 (output_file+
".goto-cc-saved").c_str());
296 error() <<
"Rename failed: " << std::strerror(errno) <<
eom;
304 debug() <<
"merging " << output_file <<
eom;
305 std::string saved=output_file+
".goto-cc-saved";
307 #if defined(__linux__) || defined(__FreeBSD_kernel__)
311 std::vector<std::string> objcopy_argv;
313 objcopy_argv.push_back(
"objcopy");
314 objcopy_argv.push_back(
"--remove-section=goto-cc");
315 objcopy_argv.push_back(output_file);
317 result =
run(objcopy_argv[0], objcopy_argv);
323 std::vector<std::string> objcopy_argv;
325 objcopy_argv.push_back(
"objcopy");
326 objcopy_argv.push_back(
"--add-section");
327 objcopy_argv.push_back(
"goto-cc="+saved);
328 objcopy_argv.push_back(output_file);
330 result =
run(objcopy_argv[0], objcopy_argv);
333 int remove_result=remove(saved.c_str());
336 error() <<
"Remove failed: " << std::strerror(errno) <<
eom;
341 #elif defined(__APPLE__)
345 std::vector<std::string> lipo_argv;
348 lipo_argv.push_back(
"lipo");
349 lipo_argv.push_back(output_file);
350 lipo_argv.push_back(
"-create");
351 lipo_argv.push_back(
"-arch");
352 lipo_argv.push_back(
"hppa7100LC");
353 lipo_argv.push_back(saved);
354 lipo_argv.push_back(
"-output");
355 lipo_argv.push_back(output_file);
360 int remove_result=remove(saved.c_str());
363 error() <<
"Remove failed: " << std::strerror(errno) <<
eom;
369 error() <<
"binary merging not implemented for this platform" <<
eom;
379 std::cout <<
"goto-as understands the options of as plus the following.\n\n";
const char * CBMC_VERSION
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
std::string output_file_object
mstreamt & result() const
@ COMPILE_LINK_EXECUTABLE
std::string output_file_executable
std::string get_value(char option) const
as_modet(goto_cc_cmdlinet &_cmdline, const std::string &_base_name, bool _produce_hybrid_binary)
static irep_idt this_operating_system()
std::string object_file_extension
goto_cc_cmdlinet & cmdline
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
static irep_idt this_architecture()
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
virtual 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.