Skip to content

Latest commit

 

History

History
68 lines (51 loc) · 2.78 KB

make-symbol.md

File metadata and controls

68 lines (51 loc) · 2.78 KB
Raw

Name

make-symbol -- make a symbol table for a goto binary

Synopsis

usage: make-symbol [-h] [--viewer-symbol JSON [JSON ...]]
				   [--viewer-source JSON [JSON ...]] [--goto GOTO]
				   [--wkdir WKDIR] [--srcdir SRCDIR]
				   [--files FILE [FILE ...]]
				   [--tags-method TAGS] [--verbose] [--debug]

Description

This is a front end for the symbolt module that viewer uses to represent the symbol table for a goto binary. The output is a json file that maps each symbol to a source location consisting of a file name, optional function name, and line number.

The are four methods for generating the symbol table:

  • sources: Load the json output of make-symbol itself
  • goto: Load the symbol table from a goto binary
  • ctags: Use ctags to scan source code for symbols
  • etags: Use etags to scan source code for symbols

Simple uses of make-symbol are

# Load symbol table from a json file produced by make-symbol
make-symbol --viewer-symbol symbols.json

# Load symbol table from a goto binary
make-symbol --srcdir /usr/project --wkdir /usr/project/proof \
    --goto program.goto

# Run ctags in SRCDIR on FILES defined in make-sources output
make-symbol --sources sources.json

# Run ctags in /usr/project on files function.c and .h
make-symbol --srcdir /usr/project --files function.c function.h

# Explicitly specify whether to use ctags or etags
make-symbol --sources sources.json --tags-method ctags
make-symbol --sources sources.json --tags-method etags

The goto method simply loads the symbol table found in a goto binary. This will include every symbol used in the goto binary, but will omit preprocessor definitions. We fill out this list of symbols and definitions by running ctags over the files listed in the symbol table, but definitions in the table take precedence over definitions inferred by ctags. This still omits definitions from files that list only definitions and do not contribute symbols to the symbol table.

The programs ctags and etags scan source files to produce symbol tables that are easy to use with the vi and emacs text editors. The ctags method requires Exuberant ctags from ctags.sourceforge.net that can be installed with most package managers, and the etags method requires the version of etags distributed with any recent version of emacs. We prefer ctags over etags (after checking which of ctags and etags is installed), since ctags seems more robust with oddly-formatted source code, although etags can run twice as fast as ctags on large source trees (as much as 30 seconds versus 60 seconds).

The goto method is easy and fairly complete. The ctags method is both minimal and complete when the make-sources is used to produce the file sources.json listing files for ctags to scan.

Type "make-symbol --help" for a complete list of command line options.