Condate: a Language for Checking Control Flow Graph Properties
Condate is the language used in the CFG checker available in the Condate branch.
svn co svn://gcc.gnu.org/svn/gcc/branches/condate condate cd condate mkdir build cd build ../configure --enable-languages=c,c++ --disable-bootstrap --prefix=somewhere make make install
N. Volanschi. "A portable compiler-integrated approach to permanent checking" condate-asej07.pdf. To appear in Automated Software Engineering. ISSN: 0928-8910 (print version), ISSN: 1573-7535 (electronic version). The original publication is available at www.springerlink.com. DOI: 10.1007/s10515-007-0022-4. Also available at http://mygcc.free.fr/condate-asej07.pdf
Here are some nice presentations that could serve as guides for the use of the CFG checker: