Skip to content
Snippets Groups Projects

[blog] post about quick ACSL guide for Eva

Merged [blog] post about quick ACSL guide for Eva
blog-mini-acsl into master
9 unresolved threads
Merged Andre Maroneze requested to merge blog-mini-acsl into master
9 unresolved threads
Compare
and
1 file
+ 110
− 0
Compare changes
  • Side-by-side
  • Inline
_posts/2022-04-06-eva-acsl-quick-guide.md 0 → 100644
+ 110
− 0
 
---
 
layout: post
 
author: André Maroneze (review by V. Prevosto, P. Baudin)
 
date: 2022-04-06 18:00 +0100
 
categories: acsl
 
title: "Quick ACSL Guide for Eva: a new mini-tutorial"
 
---
 
 
In 2016, a few blog posts
 
([part 1](2016/09/23/A-mini-tutorial-of-ACSL-specifications-for-Value.html),
 
[part 2](2016/09/30/A-mini-ACSL-tutorial-for-Value-part-2-functional-dependencies.html),
 
[part 3](2016/10/12/A-mini-ACSL-tutorial-for-Value-part-3-indirect-assigns.html))
 
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](https://www.frama-c.com/download/frama-c-eva-manual.pdf).
 
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](https://frama-c.com/html/acsl.html), 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](https://frama-c.com/download/acsl.pdf), just like most
 
Java programmers will never have to read the
 
[Java Language Specification](https://docs.oracle.com/javase/specs/jls/se18/html/index.html),
 
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](https://allan-blanchard.fr/frama-c-wp-tutorial.html),
 
available in English *and* French, and
 
[ACSL by Example](https://github.com/fraunhoferfokus/acsl-by-example), by
 
Gerlach et al., from Fraunhofer FOKUS. However, their target audience are
 
mainly [WP](https://frama-c.com/fc-plugins/wp.html) 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](https://www.frama-c.com/fc-plugins/metacsl.html),
 
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 <kbd>Ctrl+V</kbd> 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](https://git.frama-c.com/pub/frama-c/-/issues/new)
 
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.