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 ...