2 \defgroup goto-instrument goto-instrument
4 # Folder goto-instrument
8 The `goto-instrument/` directory contains a number of tools, one per
9 file, that are built into the `goto-instrument` program. All of them
10 take in a goto-program (produced by `goto-cc`) and either modify it or
11 perform some analysis. Examples include `nondet_static.cpp` which
12 initialises static variables to a non-deterministic value,
13 `nondet_volatile.cpp` which assigns a non-deterministic value to any
14 volatile variable before it is read and `weak_memory.h` which performs
15 the necessary transformations to reason about weak memory models. The
16 exception to the “one file for each piece of functionality” rule are the
17 program instrumentation options (mostly those given as “Safety checks”
18 in the `goto-instrument` help text) which are included in the
19 `goto-program/` directory. An example of this is
20 `goto-program/stack_depth.h` and the general rule seems to be that
21 transformations and instrumentation that `cbmc` uses should be in
22 `goto-program/`, others should be in `goto-instrument`.
24 `goto-instrument` is a very good template for new analysis tools. New
25 developers are advised to copy the directory, remove all files apart
26 from `main.*`, `parseoptions.*` and the `Makefile` and use these as the
27 skeleton of their application. The `doit()` method in `parseoptions.cpp`
28 is the preferred location for the top level control for the program.