Go to the documentation of this file.
34 static inline bool failed(
bool error_indicator)
36 return error_indicator;
40 const std::vector<std::string> &symtab_filenames,
41 const std::string &gb_filename)
46 if(!out_file.is_open())
50 std::vector<std::ifstream> symtab_files;
51 for(
auto const &symtab_filename : symtab_filenames)
53 std::ifstream symtab_file{symtab_filename};
54 if(!symtab_file.is_open())
59 symtab_files.emplace_back(std::move(symtab_file));
65 symtab_language->set_message_handler(message_handler);
69 for(std::size_t ix = 0; ix < symtab_files.size(); ++ix)
71 auto const &symtab_filename = symtab_filenames[ix];
72 auto &symtab_file = symtab_files[ix];
73 if(
failed(symtab_language->parse(symtab_file, symtab_filename)))
76 "failed to parse symbol table from file '" + symtab_filename +
"'"};
79 if(
failed(symtab_language->typecheck(symtab,
"<unused>")))
82 "failed to typecheck symbol table from file '" + symtab_filename +
"'"};
105 "expect at least one input file",
"<json-symtab-file>"};
107 std::vector<std::string> symtab_filenames =
cmdline.
args;
108 std::string gb_filename =
"a.out";
126 <<
"Usage: Purpose:\n"
128 <<
"symtab2gb [-?] [-h] [--help] show help\n"
129 "symtab2gb compile .json_symtabs\n"
130 " <json-symtab-file>+ to a single goto-binary\n"
131 " [--out <outfile>]\n\n"
132 "<json-symtab-file> a CBMC symbol table in\n"
134 "--out <outfile> specify the filename of\n"
135 " the resulting binary\n"
136 " (default: a.out)\n"
void link_goto_model(goto_modelt &dest, goto_modelt &src, message_handlert &message_handler)
virtual bool isset(char option) const
mstreamt & status() const
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.
Thrown when we can't handle something in an input source file.
void goto_convert(const codet &code, symbol_table_baset &symbol_table, goto_programt &dest, message_handlert &message_handler, const irep_idt &mode)
const char * CBMC_VERSION
std::unique_ptr< languaget > new_json_symtab_language()
symtab2gb_parse_optionst(int argc, const char *argv[])
std::string banner_string(const std::string &front_end, const std::string &version)
static bool failed(bool error_indicator)
std::string get_value(char option) const
Thrown when some external system fails unexpectedly.
#define SYMTAB2GB_OPTIONS
Document and give macros for the exit codes of CPROVER binaries.
static std::string binary(const constant_exprt &src)
static void run_symtab2gb(const std::vector< std::string > &symtab_filenames, const std::string &gb_filename)
Goto Programs with Functions.
#define CPROVER_EXIT_SUCCESS
Success indicates the required analysis has been performed without error.
Thrown when users pass incorrect command line arguments, for example passing no files to analysis or ...
symbol_tablet symbol_table
Symbol table.
std::string align_center_with_border(const std::string &text)
Utility for displaying help centered messages borderered by "* *".
#define SYMTAB2GB_OUT_FILE_OPT