Go to the documentation of this file.
59 "no binary provided for analysis",
"<binary> <args>");
65 "need to provide symbols to analyse via --symbols",
"--symbols");
71 if(core_file && breakpoint)
74 "cannot start gdb from both core-file and breakpoint",
75 "--core-file/--breakpoint");
78 if(!core_file && !breakpoint)
81 "need to provide either core-file or breakpoint for gdb",
82 "--core-file/--breakpoint");
86 const bool symtab_snapshot =
cmdline.
isset(
"symtab-snapshot");
88 if(symtab_snapshot && output_file)
91 "printing to a file is not supported for symbol table snapshot output",
100 std::vector<std::string> result =
split_string(symbol_list,
',',
true,
true);
107 "cannot read goto binary '" +
binary +
"'");
110 const goto_modelt goto_model(std::move(opt.value()));
127 std::vector<irep_idt> result_ids(result.size());
129 result.begin(), result.end(), result_ids.begin(), [](std::string &name) {
130 return irep_idt{name};
132 gdb_value_extractor.analyze_symbols(result_ids);
138 file.open(cmdline.get_value(
"output-file"));
142 output_file ? (std::ostream &)
file : (std::ostream &)
message.result();
146 symbol_tablet snapshot = gdb_value_extractor.get_snapshot_as_symbol_table();
151 std::string snapshot = gdb_value_extractor.get_snapshot_as_c_code();
176 <<
"Usage: Purpose:\n"
178 <<
" memory-analyzer [-?] [-h] [--help] show help\n"
179 <<
" memory-analyzer --version show"
181 <<
" memory-analyzer --symbols <symbol-list> <options> <binary> analyze"
184 <<
" --core-file <file> analyze from core file\n"
185 <<
" --breakpoint <breakpoint> analyze from breakpoint\n"
186 <<
" --symbols <symbol-list> list of symbols to analyze\n"
187 <<
" --symtab-snapshot output snapshot as symbol table\n"
188 <<
" --output-file <file> write snapshot to file\n"
189 <<
" --json-ui output snapshot in JSON format\n"
ui_message_handlert ui_message_handler
virtual bool isset(char option) const
mstreamt & status() const
Thrown when failing to deserialize a value from some low level format, like JSON or raw bytes.
void show_symbol_table(const symbol_tablet &symbol_table, ui_message_handlert &ui)
Low-level interface to gdb.
static const char * message(const static_verifier_resultt::statust &status)
Makes a status message string from a status.
void split_string(const std::string &s, char delim, std::vector< std::string > &result, bool strip, bool remove_empty)
const char * CBMC_VERSION
std::string banner_string(const std::string &front_end, const std::string &version)
std::string get_value(char option) const
High-level interface to gdb.
void register_language(language_factoryt factory)
Register a language Note: registering a language is required for using the functions in language_util...
#define MEMORY_ANALYZER_OPTIONS
memory_analyzer_parse_optionst(int argc, const char *argv[])
bool set(const cmdlinet &cmdline)
Document and give macros for the exit codes of CPROVER binaries.
std::unique_ptr< languaget > new_ansi_c_language()
static std::string binary(const constant_exprt &src)
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.
This code does the command line parsing for the memory-analyzer tool.
#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 "* *".