Testing Inexecutable Conditions on Input Pointers in C Programs with SANTE

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. We 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. Keywords: run-time errors, C pointers, static analysis, test generation.