Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

  • Subject: [Frama-c-discuss] ACSL by Example (version 13.1.1 for Aluminium)
  • From: jens.gerlach at fokus.fraunhofer.de (Gerlach, Jens)
  • Date: Wed, 2 Nov 2016 18:26:11 +0000
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