Static Loop Bound Analysis of C Programs Based on Flow Analysis and Abstract Interpretation

One of the important steps in processing the worst case execution time (WCET) of a program is to determine the loops upper bounds. Such bounds are crucial when verifying real-time systems. In this paper, we propose a static loop bound analysis which associates flow analysis and abstract interpretation. It considers binary operators (+, -, *, ) for the loop increment, nested loops, non-recursive function calls, simple loop conditions (==, !=,, Gt=, &&) and loop upper bound values (instead of intervals). We present the result of our analysis on the Malardalen benchmark suite and compare them to the recent work of Ermedahl et al.