Formally Expressing what a Program Should Do: the ACSL Language
Résumé
This chapter presents ACSL, the ANSI/ISO C Specification Language, focusing
on its current implementation within the Frama-C framework. As its name suggests,
ACSL is meant to express precisely and unambiguously the expected behavior of
a piece of C code. It plays a central role in Frama-C, as nearly all plug-ins
eventually manipulate ACSL specifications, either to generate properties that
are to be verified, or to assess that the code is conforming to these specifications.
It is thus very important to have a clear view of ACSL's semantics in order to
be sure that what you check with Frama-C is really what you mean. This chapter describes the
language in an agnostic way, independently of the various verification plug-ins that
are implemented in the platform, which are described in more details in other chapters.
It contains many examples and exercises that introduce the main features of the language
and insists on the most common pitfalls that users, even experienced ones, may encounter.