Context Generation from Formal Specifications for C Analysis Tools

TL;DR

This paper introduces a method to automatically generate analysis contexts for C functions from formal specifications, improving the robustness and efficiency of analysis tools like Frama-C in industrial applications.

Contribution

It presents a systematic approach to generate contexts from ACSL specifications, integrated into a new Frama-C plug-in for industrial use.

Findings

Successfully implemented in a new Frama-C plug-in

Applied to a subset of ACSL for context generation

Used in an operational industrial setting

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.