Combining Frama-C and PathCrawler for C Program Debugging

Software validation remains a crucial part in software development process. Software testing accounts for about 50% of the total cost of software development. Automated software validation is aimed at reducing this cost. The increasing demand has motivated much research on automated software validation. Two major techniques have improved in recent years, dynamic and static analysis. Traditionally, they were viewed as separate domains. Static analysis examines program code and reasons over all possible behaviors that might arise at run time. It is often necessary to use approximations. Static analysis is conservative and sound: the results may be weaker than desirable, but they are guaranteed to generalize to all executions. Dynamic analysis operates by executing a program and observing this execution. Dynamic analysis is efficient and precise because no approximation or abstraction needs to be done: the analysis can examine the actual, exact run-time behavior of the program for the corresponding test case. It can be as fast as program execution. The pros and cons of the two techniques are apparent. If dynamic analysis detects an error then the error is real. However, it cannot in general prove the absence of errors. On the other hand, if static analysis reports a potential error, it may be a false alarm. However, if it does not find any error (of a particular kind) in the overapproximation of program behaviors then the analyzed program clearly cannot contain such errors. Recently, there has been much interest in combining dynamic and static methods for program verification. Static and dynamic analyses can enhance each other by providing valuable information that would otherwise be unavailable. This paper reports on an ongoing project that aims to provide a new combination of static analysis and structural testing of C programs. We implement our method using two existing tools: FramaC, a framework for static analysis of C programs, and PathCrawler, a structural test generation tool. Frama-C [1] is being developed in collaboration between CEA LIST and the ProVal project of INRIA Saclay. Its software architecture is plug-in-oriented and allows finegrained collaboration of analysis techniques. Static analyzers are implemented as plugins and can collaborate with one another to examine a C program. Let us introduce the value analysis plug-in based on abstract interpretation. This plug-in computes and stores supersets of possible value ranges of variables at each statement of the program. Among Groupe de travail MTV2