Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] New Frama-C Plug-in: E-ACSL

  • Subject: [Frama-c-discuss] New Frama-C Plug-in: E-ACSL
  • From: Julien.Signoles at cea.fr (Julien Signoles)
  • Date: Mon, 09 Jan 2012 09:06:21 +0100
Hello and happy new year,

I'm glad to announce that a new Frama-C plug-in, called E-ACSL, is 
available:

	http://frama-c.com/download/e-acsl/e-acsl-0.1.tar.gz

This plug-in takes as input an annotated C program and returns the same 
program in which annotations have been converted into C code dedicated 
to runtime assertion checking: this code fails at runtime if and only if 
the annotation is violated at runtime.

Annotations must be written in a subset of ACSL, namely E-ACSL 
(Executable ANSI/ISO C Specification Language). The reference manual of 
this specification language is available at:

	http://frama-c.com/download/e-acsl/e-acsl.pdf.

This plug-in is still in a preliminary state. Which parts of E-ACSL are 
not yet implemented is described at:

	http://frama-c.com/download/e-acsl/e-acsl-implementation.pdf.

Usage and examples may be found in the tarball or on the E-ACSL's webpage:

	http://frama-c.com/eacsl.html.

This work is supported by the FUI9 `Hi-Lite' project 
(http://www.open-do.org/projects/hi-lite).

Enjoy this plug-in and do not hesitate to report your feedback.

Best wishes,
Julien Signoles