Abstract

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.

In

Guide to Software Verification with Frama-C. ISBN 978-3-031-55608-1

DOI: 10.1007/978-3-031-55608-1_1