--- layout: fc_discuss_archives title: Message 14 from Frama-C-discuss on January 2017 ---
Dear Frama-C users, The Verification Group at Fraunhofer FOKUS has just released a new version (14.1.0) of âACSL by Exampleâ. This version is intended for Frama-C Silicon. The document can be accessed through http://www.fokus.fraunhofer.de/download/acsl_by_example The examples can be accessed via git through https://gitlab.fokus.fraunhofer.de/verification/open-acslbyexample.git The most notable changes of this version are ⢠use label Old instead of Pre in function contracts ⨠⢠add algorithm rotate ⨠⢠rewrite definition of predicates EqualRanges and Reverse and provide more overloaded versions ⨠⢠add figures for algorithms rotate and replace_copy ⨠⢠update figure for predicate Reverse ⨠⢠update Coq proofs and add table with more information on the ACSL lemmas that had to be verified with Coq ⨠We hope this document helps you in your work with Frama-C/WP. Regards Jens Gerlach -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20170113/915eeee3/attachment.html>