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

memory-analyzer-5.59.0                              June 2022                                 MEMORY-ANALYZER(1)