Specification and Verification of High-Level Properties

The ACSL specification language allows the verification engineer to specify almost any property they might want to verify at any given point in a given C program. For some complex properties, it can sometimes be done at the price of an extremely complex encoding, which could quickly become error-prone if written manually. To facilitate this task, a certain number of Frama-C plug-ins offer dedicated specification languages, targeting different kinds of properties, that are then translated into a set of ACSL annotations amenable to verification via the core analysis plug-ins (EvaEva , WpWp , E-ACSLE-ACSL ). In this chapter, we present three such plug-ins. The first of them, MetAcslMetAcsl , is dedicated to pervasive properties that must be checked at each program point meeting some characteristics, for instance at each write access. A single MetAcslMetAcsl annotation can thus be instantiated by a very large number of ACSL clauses. Second, RPPRPP targets relational properties. In contrast to an ACSL function contract, which specifies what happens during a single function call, relational properties express relations over several calls of potentially different functions. Finally, AoraïAoraï is dedicated to properties over sequences of function calls that can occur during an execution.