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