Overview
GMC is an explicit-state code model checker for C/C++ programs. GMC is able to discover low-level programming errors such as buffer overflows, memory leaks, null-pointerdereferrence etc. GMC understands threads and executes all possible interleavings to discover errors manifested only in certain thread schedules. In particular, GMC understands the pthread library, but offers a means to extend the support for other thread libraries.
GMC's input is GIMPLE, the intermediate representation of the GNU Compiler Collection - GCC (gcc.gnu.org). This architecture affords compatibility with majority of open source projects and easy interation into an existing make-based compilation toolchain.
In order to fight state explosion, GMC supports basic partial order reduction as well as incremental heap cannonicalization (based on paper M. Musuvathi and D. L. Dill: An Incremental Heap Canonicalization Algorithm).
Authors
- Jan Kouba
- Ondrej Krč-Jediný
- Ondřej Šerý
Contributors
- David Hauzar
- Pavel Jančík
- Jan Kofroň
- Tomáš Poch