cprover
goto-cc/README.md
Go to the documentation of this file.
1 \ingroup module_hidden
2 \defgroup goto-cc goto-cc
3 
4 # Folder goto-cc
5 
6 \author Martin Brain
7 
8 `goto-cc` is a compiler replacement that just performs the first step of
9 the process; converting C or C++ programs to goto-binaries. It is
10 intended to be dropped in to an existing build procedure in place of the
11 compiler, thus it emulates flags that would affect the semantics of the
12 code produced. Which set of flags are emulated depends on the naming of
13 the `goto-cc/` binary. If it is called `goto-cc` then it emulates GCC
14 flags, `goto-armcc` emulates the ARM compiler, `goto-cl` emulates VCC
15 and `goto-cw` emulates the Code Warrior compiler. The output of this
16 tool can then be used with `cbmc` or `goto-instrument`.