--- layout: fc_discuss_archives title: Message 2 from Frama-C-discuss on January 2012 ---
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