Loop Patterns in C Programs

Abstract

In this work, we conduct a systematic study of loops in C programs. We describe static analyses capable of efficiently identifying definite iteration in C code. Our experiments show that over one third of loops in our benchmarks take this form. To cover further loops, we systematically weaken our definition of definite iteration and derive a family of loop classes that are heuristics for definite iteration. We then measure the occurrence of these classes on real-world C code and investigate which statements are used to express them. Finally, we empirically show that our classification is meaningful -- (a) it describes the majority of loops in our benchmarks, (b) the classes are good heuristics for termination, and (c) they can be used as software metrics to characterize benchmarks for software verification.