17 #define EX_SOFTWARE 70 36 const std::string &base_name)
38 if(cmdline.
isset(
"native-assembler"))
39 return cmdline.
get_value(
"native-assembler");
41 if(base_name==
"as86" ||
42 base_name.find(
"goto-as86")!=std::string::npos)
47 if(
pos==std::string::npos)
50 std::string result=base_name;
51 result.replace(
pos, 7,
"as");
58 const std::string &_base_name,
59 bool _produce_hybrid_binary):
61 produce_hybrid_binary(_produce_hybrid_binary),
78 base_name.find(
"goto-as86")!=std::string::npos;
84 status() <<
"as86 version: 0.16.17 (goto-cc " CBMC_VERSION
")" 87 status() <<
"GNU assembler version 2.20.51.0.7 20100318" 88 <<
" (goto-cc " CBMC_VERSION
")" <<
eom;
91 "Copyright (C) 2006-2014 Daniel Kroening, Christoph Wintersteiger\n" <<
92 "CBMC version: " CBMC_VERSION <<
'\n' <<
107 debug() <<
"AS86 mode (hybrid)" <<
eom;
114 debug() <<
"AS mode (hybrid)" <<
eom;
128 debug() <<
"Compiling and linking an executable" <<
eom;
133 debug() <<
"Compiling and linking a library" <<
eom;
138 compiler.object_file_extension=
"o";
152 compiler.output_file_object=
"a.out";
153 compiler.output_file_executable=
"a.out";
160 for(goto_cc_cmdlinet::parsed_argvt::iterator
165 if(!arg_it->is_infile_name)
170 std::ifstream is(infile);
173 error() <<
"Failed to open input source " << infile <<
eom;
184 const std::string comment2=act_as_as86 ?
"::" :
"##";
188 while(std::getline(is, line))
190 if(line==comment2+
" GOTO-CC")
194 assert(!dest.empty());
195 compiler.add_input_file(dest);
200 std::string new_name=
203 dest=temp_dir(new_name);
208 error() <<
"Failed to tmp output file " << dest <<
eom;
218 os << line.substr(2) <<
'\n';
223 assert(!dest.empty());
224 compiler.add_input_file(dest);
227 warning() <<
"No GOTO-CC section found in " << arg_it->arg <<
eom;
232 if(compiler.source_files.empty())
253 std::vector<std::string> new_argv;
256 new_argv.push_back(a.arg);
263 for(std::size_t i=0; i<new_argv.size(); i++)
264 std::cout <<
" " << new_argv[i];
273 std::string output_file=
"a.out";
282 if(output_file==
"/dev/null")
286 <<
" to generate hybrid binary" <<
eom;
291 (output_file+
".goto-cc-saved").c_str());
294 error() <<
"Rename failed: " << std::strerror(errno) <<
eom;
302 debug() <<
"merging " << output_file <<
eom;
303 std::string saved=output_file+
".goto-cc-saved";
309 std::vector<std::string> objcopy_argv;
311 objcopy_argv.push_back(
"objcopy");
312 objcopy_argv.push_back(
"--remove-section=goto-cc");
313 objcopy_argv.push_back(output_file);
315 result =
run(objcopy_argv[0], objcopy_argv);
321 std::vector<std::string> objcopy_argv;
323 objcopy_argv.push_back(
"objcopy");
324 objcopy_argv.push_back(
"--add-section");
325 objcopy_argv.push_back(
"goto-cc="+saved);
326 objcopy_argv.push_back(output_file);
328 result =
run(objcopy_argv[0], objcopy_argv);
331 int remove_result=
remove(saved.c_str());
334 error() <<
"Remove failed: " << std::strerror(errno) <<
eom;
339 #elif defined(__APPLE__) 343 std::vector<std::string> lipo_argv;
346 lipo_argv.push_back(
"lipo");
347 lipo_argv.push_back(output_file);
348 lipo_argv.push_back(
"-create");
349 lipo_argv.push_back(
"-arch");
350 lipo_argv.push_back(
"hppa7100LC");
351 lipo_argv.push_back(saved);
352 lipo_argv.push_back(
"-output");
353 lipo_argv.push_back(output_file);
358 int remove_result=
remove(saved.c_str());
361 error() <<
"Remove failed: " << std::strerror(errno) <<
eom;
367 error() <<
"binary merging not implemented for this platform" <<
eom;
377 std::cout <<
"goto-as understands the options of as plus the following.\n\n";
struct configt::ansi_ct ansi_c
virtual int doit()
does it.
int run(const std::string &what, const std::vector< std::string > &argv, const std::string &std_input, const std::string &std_output, const std::string &std_error)
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...
std::string get_value(char option) const
unsignedbv_typet size_type()
const bool produce_hybrid_binary
static mstreamt & eom(mstreamt &m)
std::string get_base_name(const std::string &in, bool strip_suffix)
cleans a filename from path and extension
mstreamt & warning() const
bool set(const cmdlinet &cmdline)
virtual bool isset(char option) const
goto_cc_cmdlinet & cmdline
static std::string assembler_name(const cmdlinet &cmdline, const std::string &base_name)
Compile and link source and object files.
static irep_idt this_operating_system()
virtual void help_mode()
display command line help
mstreamt & result() const
gcc_message_handlert message_handler
mstreamt & status() const
virtual void help()
display command line help
as_modet(goto_cc_cmdlinet &_cmdline, const std::string &_base_name, bool _produce_hybrid_binary)
std::string to_string(const string_constraintt &expr)
Used for debug printing.
int run_as()
run as or as86 with original command line
goto_programt coverage_criteriont message_handlert & message_handler
const std::string native_tool_name
const std::string base_name
static irep_idt this_architecture()