A Late Treatment of C Precondition in Dynamic Symbolic Execution
Mickaël Delahaye, Nikolaï Kosmatov · 2013
Relevance of automatically generated test cases depends on an appropriate definition of a test context, or precondition. This paper presents a novel method for handling a precondition in dynamic symbolic execution (DSE) testing tools. This method allows PathCrawler, a DSE tool for C programs, to accept a precondition defined as a C function. It provides a simple way to express a precondition even for developers who are not familiar with specification formalisms. It has also proven useful when combining static and dynamic analysis.