Condate: a Language for Checking Control Flow Graph Properties
Condate is the language used in the CFG checker available in the Condate branch.
Build instructions
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
Related work
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:
An Introduction to MyGCC: Abe_Skolnik___Presentation_1_.pdf
How MyGCC Works And How You Can Use It: Abe_Skolnik___Presentation_2_.pdf
A Critical Analysis of MyGCC: Abe_Skolnik___Presentation_3_.pdf
Final paper: Abe_Skolnik___Paper.pdf