Title: Context Generation from Formal Specifications for C Analysis Tools,
Abstract: Analysis tools like abstract interpreters, symbolic execution tools and
testing tools usually require a proper context to give useful results when
analyzing a particular function. Such a context initializes the function
parameters and global variables to comply with function requirements. However
it may be error-prone to write it by hand: the handwritten context might
contain bugs or not match the intended specification. A more robust approach is
to specify the context in a dedicated specification language, and hold the
analysis tools to support it properly. This may mean to put significant
development efforts for enhancing the tools, something that is often not
feasible if ever possible.
This paper presents a way to systematically generate such a context from a
formal specification of a C function. This is applied to a subset of the ACSL
specification language in order to generate suitable contexts for the abstract
interpretation-based value analysis plug-ins of Frama-C, a framework for
analysis of code written in C. The idea here presented has been implemented in
a new Frama-C plug-in which is currently in use in an operational industrial
setting.