--- layout: fc_discuss_archives title: Message 2 from Frama-C-discuss on November 2016 ---
Dear Frama-C users, The Verification Group at Fraunhofer FOKUS has just released a new version (13.1.1) of âACSL by Exampleâ. 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 - improve layout of tables of verification results - use two additional automatic theorem provers (CVC3 and E) - non-mutating algorithms - add algorithm find_end - add definition of predicate HasSubRange on subranges - add definition of predicate EqualRanges on subranges - rename lemma HasSubRange_fit_size to HasSubRangeSize - rename lemma HasConstantSubRange_fit_size to HasSubRangeSize - rename logic function CountSection to Count (using overloading in ACSL) - add lemma HasValueCountInversion - add lemma HasValueShiftInversion - add lemma CountShift - mutating algorithms - add algorithm copy_backward - relax precondition on separation of copy, replace_copy and remove_copy - provide a more sophisticated implementation of remove - re-introduceasecondversionofremove_copy that also specifies the stability of the algorithm - add algorithm random_shuffle We hope this document helps you in your work with Frama-C/WP. Regards Jens Gerlach