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

[Frama-c-discuss] New release of E-ACSL



Dear Frama-C users,

I am please to announce a new major release of the plug-in E-ACSL for Frama-C
Silicon:

     http://frama-c.com/download/e-acsl/e-acsl-0.8.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 for runtime
assertion checking: this code fails at runtime whenever an annotation is
violated. More information is available at:

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

The main highlights of this release are:
- compatibility with Frama-C Silicon
- a new E-ACSL run-time library based on shadow memory: one order of magnitude faster than before when checking memory accesses!
- better efficiency when checking properties over integers
- significant improvements to the e-acsl-gcc.sh wrapper script
- reporting of stack-traces when detecting a failure at runtime
- several bugfixes

A comprehensive list of changes is available in the tarball.

I would like to thank Kostyantyn Vorobyov who is the main contributor to this release.

Best regards,
Julien Signoles
-------------- section suivante --------------
Une pièce jointe HTML a été nettoyée...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20170118/0d97b04f/attachment.html>