--- layout: fc_discuss_archives title: Message 2 from Frama-C-discuss on November 2016 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] ACSL by Example (version 13.1.1 for Aluminium)



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