Termination Analysis of C Programs Using Compiler Intermediate Languages

摘要

Modeling the semantics of programming languages like C for theautomated termination analysis of programs is a challenge if completecoverage of all language features should be achieved. On the otherhand, low-level intermediate languages that occur during thecompilation of C programs to machine code have a much simplersemantics since most of the intricacies of C are taken care of by thecompiler frontend. It is thus a promising approach to use theseintermediate languages for the automated termination analysis of Cprograms. In this paper we present the tool KITTeL based on thisapproach. For this, programs in the compiler intermediate languageare translated into term rewrite systems (TRSs), and the terminationproof itself is then performed on the automatically generated TRS. Anevaluation on a large collection of C programs shows the effectivenessand practicality of KITTeL on "typical" examples.