 |
Compiling GOTO-Programs |
|
About ― Download ― Examples ― Documentation
About goto-cc
goto-cc is
a compiler that compiles programs given in a multitude of
programming languages (mostly C and C++) into GOTO-programs. This is
done in a gcc-compliant style, which means that you can replace
gcc in your makefiles or configure scripts with goto-cc and obtain a
GOTO-binary instead of a real binary. The resulting goto-binaries
can then easily be used with verification tools like SATABS or CBMC.
As additional feature, it generates dot
-style flowgraphs of your functions!
For questions about goto-cc, contact
Christoph M. Wintersteiger.
You should also read the license. |  |
goto-cc News
| 02-01-2009: | Version 2.7 released. The header of goto-binaries has changed; to avoid problems, please recompile your binaries. Get it from the downloads page. | |
| 11-11-2009: | Version 2.6.2 released; bugfix release. | |
| 11-02-2009: | Version 2.6.1 released; bugfix release. | |
| 09-29-2009: | Version 2.6 released. This release features an optimized binary model format. To avoid problems, recompile please! | |
| 03-19-2009: | Version 2.5.3 released; bugfix release. | |
| 02-17-2008: | Version 2.5.2 released. This is a bugfix release. | |
| 11-05-2007: | Version 2.5.1 released. This is a bugfix release. | |
| 05-23-2007: | Version 2.5 released. More front-end fixes
and we switched to a binary
format. Don't forget to update to the new versions of
our modelcheckers that can read this format! | |
| 03-01-2007: | Version 2.1.2 released. Minor bug fixes. | |
| 02-02-2007: | Version 2.1.1 released. Minor bug fixes. | |
| 01-28-2007: | Version 2.1 released. Major front-end overhaul, library linking fully in place now. | |
| 10-26-2006: | Version 2.0.1 released (minor bugfixes). | |
| 09-13-2006: | Version 2.0 released. | |
| 07-10-2006: | First public version released. |
Support
This research is currently supported by an award from IBM research
and a grant from the Swiss
National Science Foundation.