Common specification language for static and dynamic analysis of C programs

Abstract

Various combinations of static and dynamic analysis techniques were recently shown to be beneficial for software verification. A frequent obstacle to combining different tools in a completely automatic way is the lack of a common specification language. Our work proposes to translate a Pre-Post based specification into executable C code. This paper presents e-acsl, subset of the acsl specification language for C programs, and its automatic translator into C implemented as a Frama-C plug-in. The resulting C code is executable and can be used by a dynamic analysis tool. We illustrate how the PathCrawler test generation tool automatically treats such pre- and postconditions specified as C functions.