RTL-check is a framework for static analysis of programs from a safety and security perspective. It performs analysis on RTL, which is the low-level intermediate representation generated by GCC. This framework was created for a research project that deals with static analysis and memory safety of programs developed in unsafe languages such as C or C++. In particular, it is targeted at detecting buffer overflows statically and proving their absence. However, this framework should be useful for other projects dealing with static analysis.
