--- layout: fc_discuss_archives title: Message 36 from Frama-C-discuss on May 2013 ---
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