Compiler_Implementation

GNAT2GOTO Implementation

GNAT2GOTO is implemented as a backend to the GNAT Ada Compiler. Most of the code lives in the driver directory, where the entry point for gnat2goto is the back_end.adb - this file, together driver.adb contain the setup code needed for the GNAT parts of GNAT2GOTO.

The data definitions for the Ada representation GOTO programs can be found in the ireps directory, where they are being autogenerated from specifications in ireps/specs with the ireps_generator.py script.

The translation of Ada AST nodes (supplied by the GNAT frontend) to GOTO Ireps happens in driver/tree_walk.adb. In here, the AST is recursively traversed (the entry point being Do_Compilation_Unit) and equivalent GOTO programs are generated. See the CProver documentation for a short overview of the structure of GOTO programs. In short, the output of the Tree_Walk routine is a Symbol_Table containing global variables, functions, types etc representing the same semantics as the original Ada program. The contents of this symbol table are then output as a .json_symtab file which can be read by the cbmc program (as of now this requires a patch to cbmc that will hopefully be part of mainline cbmc, right now it can be found here).