Folder Walkthrough

Author

Martin Brain, Peter Schrammel

<tt>src/</tt>

The source code is divided into a number of sub-directories, each containing the code for a different part of the system.

• GOTO-Programs
  • goto-programs
  • linking
• Symbolic Execution
  • goto-checker
  • goto-symex
• Static Analyses
  • analyses
  • pointer-analysis
• Solvers
  • solvers
• Language Front Ends
  • Language API: langapi
  • C: ansi-c
  • C++: cpp
  • Java: java_bytecode
• Tools
  • cbmc
  • goto-analyzer
  • goto-cc
  • goto-diff
  • goto-harness
  • goto-instrument
  • jbmc
• Utilities
  • big-int
  • json
  • xmllang
  • util
  • miniz

In the top level of src there are only a few files:

• config.inc: The user-editable configuration parameters for the build process. The main use of this file is setting the paths for the various external SAT solvers that are used. As such, anyone building from source will likely need to edit this.
• Makefile: The main systems Make file. Parallel builds are supported and encouraged; please don’t break them!
• common: System specific magic required to get the system to build. This should only need to be edited if porting CBMC to a new platform / build environment.
• doxygen.cfg: The config file for doxygen.cfg

<tt>doc/</tt>

Contains the CBMC man page. Doxygen HTML pages are generated into the doc/html directory when running doxygen from src.

<tt>regression/</tt>

The regression/ directory contains the regression test suites. See Compilation and Development for information on how to run and develop regression tests.

<tt>unit/</tt>

The unit/ directory contains the unit test suites. See Compilation and Development for information on how to run and develop unit tests.

Directory dependencies

This diagram shows intended directory dependencies. Arrows should be read transitively - dependencies of dependencies are often used directly.

There are module_dependencies.txt files in each directory, which are checked by the linter. Where directories in module_dependencies.txt are marked with comments such as 'dubious' or 'should go away', these dependencies have generally not been included in the diagram.

Last modified: 2024-11-20 06:00:32 -0800