• Condate

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