--- layout: fc_discuss_archives title: Message 2 from Frama-C-discuss on January 2012 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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



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