cprover
Goto Conversion & Instrumentation
Author
Kareem Khazem

Goto Conversion

In the goto-programs directory.

Key classes:

At this stage, CBMC constructs a goto-program from a symbol table. It does not use the parse tree or the source file at all for this step. This may seem surprising, because the symbols are stored in a hash table and therefore have no intrinsic order; nevertheless, every symbolt is associated with a source_locationt, allowing CBMC to figure out the lexical order.

The structure of what is informally called a goto-program follows. The entire target program is converted to a single goto_functionst object. The goto functions contains a set of goto_programt objects; each of these correspond to a "function" or "method" in the target program. Each goto_program contains a list of instructions; each instruction contains an associated statement—these are subtypes of codet. Each instruction also contains a "target", which will be empty for now.

This is not the final form of the goto-functions, since the lists of instructions will be 'normalized' in the next step (Instrumentation), which removes some instructions and adds targets to others.

Note that goto_programt and goto_functionst are each template instantiations; they are currently the only specialization of goto_program_templatet and goto_functions_templatet, respectively. This means that the generated Doxygen documentation can be somewhat obtuse about the actual types of things, and is unable to generate links to the correct classes. Note that the code member of a goto_programt's instruction has type codet (its type in the goto_program_templatet documentation is given as "codeT", as this is the name of the template's type parameter); similarly, the type of a guard of an instruction is guardt.


Instrumentation

In the goto-programs directory.

Key classes:

This stage applies several transformations to the goto-programs from the previous stage:

This stage concludes the analysis-independent program transformations.