--- layout: fc_discuss_archives title: Message 9 from Frama-C-discuss on June 2017 ---
Dear Frama-C users, The Verification Group at Fraunhofer FOKUS has released a new version (15.1.0) of âACSL by Exampleâ. This version is intended for Frama-C 15 (Phosporus). Starting with this release you the PDF documentation and the examples are hosted at GitHub https://github.com/fraunhoferfokus/acsl-by-example The document can be directly accessed through https://github.com/fraunhoferfokus/acsl-by-example/blob/master/ACSL-by-Example.pdf The most notable changes of this version are - The verification results are now part of the appendix. - Fix an error in the specification of the well-definition of stack_size. - This release of Frama-C/WP could not discharge some of our assertions of push_heap. We therefore have completely rewritten the annotations and also tweaked the implementation of push_heap. We also added some new predicates and lemmas to maintain a concise specification that can easily be verified by automatic provers. * add predicate MultisetAdd and lemma MultisetAddDistinct * add predicate MultisetMinus and lemma MultisetMinusDistinct * add predicate MultisetRetain and lemma MultisetPushHeapRetain * provide an additional version of predicate MultisetRetainRest * and lemma MultisetPushHeapClosure We hope this document helps you in your work with Frama-C/WP. Regards Jens Gerlach