41 message(ui_message_handler)
65 "no binary provided for analysis",
"<binary> <args>");
71 "need to provide symbols to analyse via --symbols",
"--symbols");
77 if(core_file && breakpoint)
80 "cannot start gdb from both core-file and breakpoint",
81 "--core-file/--breakpoint");
84 if(!core_file && !breakpoint)
87 "need to provide either core-file or breakpoint for gdb",
88 "--core-file/--breakpoint");
92 const bool symtab_snapshot =
cmdline.
isset(
"symtab-snapshot");
94 if(symtab_snapshot && output_file)
97 "printing to a file is not supported for symbol table snapshot output",
110 "cannot read goto binary '" +
binary +
"'");
141 output_file ? (std::ostream &)file : (std::ostream &)
message.
result();
177 "Usage: \tPurpose:\n"
179 " {bmemory-analyzer} [{y-?}] [{y-h}] [{y--help}] \t show this help\n"
180 " {bmemory-analyzer} {y--version} \t show version\n"
181 " {bmemory-analyzer} [options] {y--symbols} {usymbol-list} {ubinary} \t"
182 " analyze {ubinary}\n"
185 " {y--core-file} {ufile_name} \t analyze from core file {ufile_name}\n"
186 " {y--breakpoint} {uname} \t analyze from breakpoint {uname}\n"
187 " {y--symbols} {usymbol-list} \t list of symbols to analyze\n"
188 " {y--symtab-snapshot} \t output snapshot as symbol table\n"
189 " {y--output-file} {ufile_name} \t write snapshot to file {ufile_name}\n"
190 " {y--json-ui} \t output snapshot in JSON format\n"
High-level interface to gdb.
std::unique_ptr< languaget > new_ansi_c_language()
std::string get_value(char option) const
virtual bool isset(char option) const
std::list< std::string > get_comma_separated_values(const char *option) const
Collect all occurrences of option option and split their values on each comma, merging them into a si...
bool set(const cmdlinet &cmdline)
Thrown when failing to deserialize a value from some low level format, like JSON or raw bytes.
symbol_tablet symbol_table
Symbol table.
Thrown when users pass incorrect command line arguments, for example passing no files to analysis or ...
memory_analyzer_parse_optionst(int argc, const char *argv[])
void register_languages() override
mstreamt & result() const
ui_message_handlert ui_message_handler
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.
static std::string binary(const constant_exprt &src)
This code does the command line parsing for the memory-analyzer tool.
#define MEMORY_ANALYZER_OPTIONS
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 bool read_goto_binary(const std::string &filename, symbol_tablet &, goto_functionst &, message_handlert &)
Read a goto binary from a file, but do not update config.
void show_symbol_table(const symbol_table_baset &symbol_table, ui_message_handlert &ui)
const char * CBMC_VERSION