A Formal Semantics of C With Applications
This paper describes an executable formal semantics of C expressed using a formalism based on term rewriting. Being executable, the semantics has been thoroughly tested against the GCC torture test suite and successfully passes over 96% of 715 test programs. It is the most complete and thoroughly tested formal definition of C to date. The semantics yields an interpreter, debugger, and state space search tool "For free". The semantics is shown capable of automatically finding program errors, both statically and at run-time. It is also used to enumerate non-deterministic behavior. These techniques together allow the tool to identify undefined programs. The entire C semantics is included as Appendix B.