Date Added: Jul 2012
Combinations of static and dynamic analysis techniques make it possible to detect the risk of out-of-bounds memory access in C programs and to confirm it on concrete test data. However, this is not directly possible for input arrays/pointers in C functions. This paper presents a specific technique allowing the interpretation and execution of assertions involving the size of an input array (pointer) of a C function. The authors show how this technique was successfully exploited in the SANTE tool where it allowed potential out-of-bounds access errors to be detected and classified in several real-life programs.