cprover
|
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.
In the goto-programs directory.
Key classes:
This stage applies several transformations to the goto-programs from the previous stage:
code_ifthenelset is turned into GOTOs. In particular, the bodies of the conditionals are flattened into lists of instructions, inline with the rest of the instruction in the goto_programt. The guard of the conditional is placed onto the guard member of an instruction whose code member is of type code_gotot. The targets member of that instruction points to the appropriate branch of the conditional. (Note that although instructions have a list of targets, in practice an instruction should only ever have at most one target; you should check this invariant with an assertion if you rely on it).
The order of instructions in a list of instructions—as well as the targets of GOTOs—are both displayed as arrows when viewing a goto-program as a Graphviz DOT file with goto-instrument --dot
. The semantics of a goto-program is: the next instruction is the next instruction in the list, unless the current instruction has a target; in that case, check the guard of the instruction, and jump to the target if the guard evaluates to true.
This stage concludes the analysis-independent program transformations.