Quick ACSL Guide for Eva: a new mini-tutorial

In 2016, a few blog posts (part 1, part 2, part 3) presented a short tutorial on writing ACSL clauses for Eva (back then, the Value Analysis plug-in). A few things changed since then, but posting them again in this blog would lead to the same issue in the future. Instead, we added an annex to the Eva user manual. This annex, titled ACSL Quick Guide for Eva, is targeted towards a slightly different audience, including complete ACSL beginners. In this blog post, we present the annex, its motivation, and summarize its most interesting contents.

Yet Another ACSL Tutorial?

ACSL, the ANSI/ISO C Language, the lingua franca of Frama-C, is important for most, if not all, Frama-C users. Fortunately, most users will never (or rarely) need to read the ACSL reference manual, just like most Java programmers will never have to read the Java Language Specification, and most C programmers… well, most C programmers should read the C standard, just to realize how deep the madness goes. But I digress.

ACSL has currently at least 2 excellent guides: Blanchard’s WP tutorial, available in English and French, and ACSL by Example, by Gerlach et al., from Fraunhofer FOKUS. However, their target audience are mainly WP users, who fell into the loop invariant cauldron when they were a baby. These guides must be as thorough as possible, since their users will need to not only read but also write lots of ACSL (except if they are using MetAcsl, of course). For the fledging Eva user, who wants mostly to pretend that ACSL does not exist and just keep on verifying their code as automatically as they can (with Frama-C as inconspicuous as possible), such guides are more than they need.

This is one of the motivations of the original blog post series mentioned in the beginning of this post. However, industrial users over the years have shown us that those posts still require some knowledge of ACSL (it is written in the first post: Prerequisites: … Basic knowledge of ACSL). But then, where do they get such basic knowledge? From reading the ACSL language specification (oh, the horror!)? From reading one of the WP guides? But then, where do they start, and where do they stop? Should users just learn by themselves by reading Frama-C’s standard library specifications (no: this is neither the easiest nor the safest way to do so)? None of these solutions is satisfying. Hence the need for a new, zero-ACSL-required tutorial.

ACSL ∩ Eva in 10 pages

Writing a quick ACSL guide for Eva allows us to simplify the presentation and avoid content that is irrelevant for Eva, either because currently unsupported (such as some higher-level logic features), or because it never appears in the specifications used by Eva. We also designed a few sections as optional material, with predicates which are sometimes seen in libc specifications (and thus potentially relevant for Eva), but not essential for first-time users. We also included sections on behaviors (not for the faint-hearted, but essential for precision and thus present in several libc specifications), dynamic memory allocation, and some unintuitive features that might confuse users. Finally, in the end, we added a FAQ/Troubleshooting/Common errors section, whose purpose is to, ideally, allow users to Ctrl+V unexpected error messages and hopefully get a direct explanation about them. This section can definitely benefit from user feedback; if you find an error message that seems too cryptic or that took you longer than necessary to understand, please consider filing an issue with the code and the message, and we’ll consider incorporating it in the guide. If you are really motivated, you can even create a merge request in our Gitlab! The Eva user manual is part of the source code of Frama-C, in directory doc/value, so everyone can contribute (at least everyone who can write in LaTeX, but here I digress again). That is also one of the benefits of putting the guide in the user manual instead of a blog post.

A few tricks up Eva’s sleeve

This quick guide is not only for new Frama-C/Eva users. It also describes a few ACSL details specific to Eva, which explain some specification choices and may help users understand why some cases are not handled by Eva as one would expect. The main one is the indirect: label in some \from clauses, which is currently only used by Eva (but very helpful in avoiding the production of garbled mix). The difference between disjunctions with holes and interval-like disjunctions (e.g. a != 0 creates a single interval with 0 as a “hole”, while a < 0 || a > 0 creates two intervals without holes) is also specific to Eva, and earns a mention in the guide.

Conclusion

We expect this guide to be especially useful for new Frama-C/Eva users, who have never seen ACSL before and would like to start using Eva as quickly as possible, without having to invest too much time into learning. Of course, code relying heavily on C standard library files, or requiring stubs for complex reasoning, will always require some effort; but lowering that effort is one of the objectives of Frama-C: showing that formal methods can be efficiently applied at industrial scale, to cope with this ineffable language that is C.