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