39static inline bool failed(
bool error_indicator)
41 return error_indicator;
45 const std::vector<std::string> &symtab_filenames,
46 const std::string &gb_filename)
51 if(!out_file.is_open())
55 std::vector<std::ifstream> symtab_files;
56 for(
auto const &symtab_filename : symtab_filenames)
58 std::ifstream symtab_file{symtab_filename};
59 if(!symtab_file.is_open())
64 symtab_files.emplace_back(std::move(symtab_file));
70 symtab_language->set_message_handler(message_handler);
74 for(std::size_t ix = 0; ix < symtab_files.size(); ++ix)
76 auto const &symtab_filename = symtab_filenames[ix];
77 auto &symtab_file = symtab_files[ix];
78 if(
failed(symtab_language->parse(symtab_file, symtab_filename)))
81 "failed to parse symbol table from file '" + symtab_filename +
"'"};
84 if(
failed(symtab_language->typecheck(symtab,
"<unused>")))
87 "failed to typecheck symbol table from file '" + symtab_filename +
"'"};
91 if(
failed(
linking(linked_symbol_table, symtab, message_handler)))
94 symtab_filename +
"'"};
127 "expect at least one input file",
"<json-symtab-file>"};
129 std::vector<std::string> symtab_filenames =
cmdline.
args;
130 std::string gb_filename =
"a.out";
150 <<
"Usage: Purpose:\n"
152 <<
"symtab2gb [-?] [-h] [--help] show help\n"
153 "symtab2gb compile .json_symtabs\n"
154 " <json-symtab-file>+ to a single goto-binary\n"
155 " [--out <outfile>]\n\n"
156 "<json-symtab-file> a CBMC symbol table in\n"
158 "--out <outfile> specify the filename of\n"
159 " the resulting binary\n"
160 " (default: a.out)\n"
std::unique_ptr< languaget > new_ansi_c_language()
std::string get_value(char option) const
virtual bool isset(char option) const
void set_from_symbol_table(const symbol_tablet &)
bool set(const cmdlinet &cmdline)
symbol_tablet symbol_table
Symbol table.
Thrown when users pass incorrect command line arguments, for example passing no files to analysis or ...
Thrown when we can't handle something in an input source file.
mstreamt & status() const
void swap(symbol_tablet &other)
Swap symbol maps between two symbol tables.
symtab2gb_parse_optionst(int argc, const char *argv[])
void register_languages() override
Thrown when some external system fails unexpectedly.
Document and give macros for the exit codes of CPROVER binaries.
#define CPROVER_EXIT_SUCCESS
Success indicates the required analysis has been performed without error.
void goto_convert(const codet &code, symbol_table_baset &symbol_table, goto_programt &dest, message_handlert &message_handler, const irep_idt &mode)
Goto Programs with Functions.
static std::string binary(const constant_exprt &src)
std::unique_ptr< languaget > new_json_symtab_language()
bool linking(symbol_tablet &dest_symbol_table, const symbol_tablet &new_symbol_table, message_handlert &message_handler)
Merges the symbol table new_symbol_table into dest_symbol_table, renaming symbols from new_symbol_tab...
void register_language(language_factoryt factory)
Register a language Note: registering a language is required for using the functions in language_util...
std::string align_center_with_border(const std::string &text)
Utility for displaying help centered messages borderered by "* *".
std::string banner_string(const std::string &front_end, const std::string &version)
static void run_symtab2gb(const std::vector< std::string > &symtab_filenames, const std::string &gb_filename)
static bool failed(bool error_indicator)
#define SYMTAB2GB_OPTIONS
#define SYMTAB2GB_OUT_FILE_OPT
const char * CBMC_VERSION
bool write_goto_binary(std::ostream &out, const symbol_tablet &symbol_table, const goto_functionst &goto_functions, irep_serializationt &irepconverter)
Writes a goto program to disc, using goto binary format.