--- layout: fc_discuss_archives title: Message 36 from Frama-C-discuss on May 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Plug-in E-ACSL 0.2 is available



Hello,

I'm glad to announce a new release of the Frama-C plug-in E-ACSL:

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

It is compatible with the recent Frama-C Fluorine (both 
Fluorine-20130401 and Fluorine-20130501).

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

Have a look at the new user manual for additional information:

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

Since version 0.1, the main changes are:
   * support of memory-related constructs like \valid and \initialized
   * prevent runtime errors in annotations
   * use GMP only when required (almost never in practice).

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

Best regards,
Julien Signoles
-- 
Researcher-engineer
CEA LIST, Software Safety Labs
tel:(+33)1.69.08.00.18  fax:(+33)1.69.08.83.95  Julien.Signoles at cea.fr