--- layout: fc_discuss_archives title: Message 44 from Frama-C-discuss on June 2015 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] E-ACSL 0.5 for Sodium



Dear Frama-C users,

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

     http://frama-c.com/download/e-acsl/e-acsl-0.5.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 Sodium
- support of \freeable, thus invalid calls to free (e.g. double free) 
are detected
- better support of literal strings

A comprehensive list of changes is available in the tarball.

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