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",
106 std::vector<std::string> result =
split_string(symbol_list,
',',
true,
true);
113 "cannot read goto binary '" +
binary +
"'");
116 const goto_modelt goto_model(std::move(opt.value()));
133 std::vector<irep_idt> result_ids(result.size());
135 result.begin(), result.end(), result_ids.begin(), [](std::string &name) {
136 return irep_idt{name};
138 gdb_value_extractor.analyze_symbols(result_ids);
144 file.open(cmdline.get_value(
"output-file"));
148 output_file ? (std::ostream &)
file : (
std::ostream &)message.result();
152 symbol_tablet snapshot = gdb_value_extractor.get_snapshot_as_symbol_table();
157 std::string snapshot = gdb_value_extractor.get_snapshot_as_c_code();
182 <<
"Usage: Purpose:\n"
184 <<
" memory-analyzer [-?] [-h] [--help] show help\n"
185 <<
" memory-analyzer --version show"
187 <<
" memory-analyzer --symbols <symbol-list> <options> <binary> analyze"
190 <<
" --core-file <file> analyze from core file\n"
191 <<
" --breakpoint <breakpoint> analyze from breakpoint\n"
192 <<
" --symbols <symbol-list> list of symbols to analyze\n"
193 <<
" --symtab-snapshot output snapshot as symbol table\n"
194 <<
" --output-file <file> write snapshot to file\n"
195 <<
" --json-ui 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
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 & status() 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_tablet &symbol_table, ui_message_handlert &ui)
void split_string(const std::string &s, char delim, std::vector< std::string > &result, bool strip, bool remove_empty)
const char * CBMC_VERSION