Blog

Tag Archives: ACSL

On Dedicated Specification Languages Beyond ACSL contracts
Virgile Prevosto on 13 June 2025

La critique du langage ne peut éluder ce fait que nos paroles nous engagent et que nous devons leur être fidèles. — Albert Camus This post was originally written for the SecOPERA project’s blog. A crucial, but often neglected aspect of formal software evaluation process, is how we specify the...

Read More

Quick ACSL Guide for Eva: a new mini-tutorial
André Maroneze (review by V. Prevosto, P. Baudin) on 6 April 2022

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....

Read More

Admit and check annotations in ACSL
André Maroneze on 10 June 2021

In Frama-C 23 (Vanadium), two new kinds of ACSL annotations are available, to complement assert: the admit and check annotations. In a nutshell, assert P is equivalent to check P; admit P. The former allows easier checking of the validity of predicates, while the latter documents the introduction of external...

Read More

Frama-C and ACSL are on GitHub
André Maroneze on 22 November 2016

We are glad to announce the creation of official GitHub repositories for Frama-C and ACSL, to stimulate contributions from the community, and to better contribute back to it. Frama-C is on GitHub Frama-C now (in fact, since a few months) has an official GitHub repository: https://github.com/Frama-C/Frama-C-snapshot It contains snapshots of...

Read More

A mini ACSL tutorial for Value, part 3: indirect assigns
André Maroneze on 12 October 2016

To conclude our 3-part series on ACSL specifications for Value, we present a feature introduced in Frama-C Aluminium that allows more precise specifications: the indirect label in ACSL assigns clauses. The expressivity gains when writing \froms are especially useful for plugins such as Value. Indirect assigns Starting in Frama-C Aluminium...

Read More