NAME¶

memory-analyzer - Snapshot program state for symbolic analysis

SYNOPSIS¶

memory-analyzer [-?] [-h] [--help]

show help

memory-analyzer --version

show version

memory-analyzer --symbols symbol_list [options] binary

analyze binary

DESCRIPTION¶

memory-analyzer is a front-end that runs and queries gdb(1) in order to obtain a snapshot of the state of an input program at a particular program location. Such a snapshot could be useful on its own: to check the values of variables at a particular program location. Furthermore, since the snapshot is a state of a valid concrete execution, it can also be used for subsequent analyses.

In order to analyze a program with memory-analyzer it needs to be compiled with goto-gcc(1). This yields an elf(5) executable that also includes a goto-cc section holding the goto model:

goto-gcc -g input_program.c -o input_program_exe
    

memory-analyzer supports two ways of running gdb(1) on user code: either to run the code from a core-file or up to a break-point. If the user already has a core-file, they can specify it with the option --core-file cf. If the user knows the point of their program from where they want to run the analysis, they can specify it with the option --breakpoint bp. Only one of core-file/break-point option can be used.

The tool also expects a comma-separated list of symbols to be analyzed via --symbols s1,s2,.... The tool invokes gdb(1) to obtain the snapshot which is why the -g option is necessary when compiling for the program symbols to be visible.

Take for example the following program:

// main.c
void checkpoint() {}
int array[] = {1, 2, 3};
int main() {


  array[1] = 4;


  checkpoint();


  return 0;
}

Say we are interested in the evaluation of array at the call-site of checkpoint. We compile the program with

goto-gcc -g main.c -o main_exe
    

And then we call memory-analyzer with:

memory-analyzer --breakpoint checkpoint --symbols array main_exe

to obtain as output the human readable list of values for each requested symbol:

{


  array = { 1, 4, 3 };
}

The above result is useful for the user and their preliminary analysis but does not contain enough information for further automated analyses. To that end, memory analyzer has an option for the snapshot to be represented in the format of a symbol table (with --symtab-snapshot). Finally, to obtain an output in JSON format, e.g., for further analyses by goto-harness(1) the additional option --json-ui needs to be passed to memory-analyzer:

memory-analyzer --symtab-snapshot --json-ui --breakpoint checkpoint


  --symbols array main_exe > snapshot.json
    

OPTIONS¶

--core-file file_name

Analyze from core dump file_name.

--breakpoint breakpoint

Analyze from given breakpoint.

--symbols symbol_list

List of symbols to analyze.

--symtab-snapshot

Output snapshot as JSON symbol table that can be used with symtab2gb(1).

--output-file file_name

Write snapshot to file_name.

--json-ui

Output snapshot in JSON format.

ENVIRONMENT¶

All tools honor the TMPDIR environment variable when generating temporary files and directories.

BUGS¶

If you encounter a problem please create an issue at https://github.com/diffblue/cbmc/issues

SEE ALSO¶

cbmc(1), elf(5), gdb(1), goto-gcc(1), goto-harness(1), symtab2gb(1)

COPYRIGHT¶

2019, Malte Mues, Diffblue