50 std::ofstream out_file{
gb_filename, std::ios::binary};
51 if(!out_file.is_open())
87 "failed to typecheck symbol table from file '" +
symtab_filename +
"'"};
127 "expect at least one input file",
"<json-symtab-file>"};
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()
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
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)
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
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.
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.