--- layout: fc_discuss_archives title: Message 33 from Frama-C-discuss on July 2018 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] ACSL by Example (version 17.2.0 for Frama-C 17, Chlorine)



Dear Frama-C users,
 
The Verification Group at Fraunhofer FOKUS has released a new version (17.2.0) of “ACSL by Example”.
This version is intended for Frama-C 17 (Chlorine-20180502). Its source can be accessed through Github
 
            https://github.com/fraunhoferfokus/acsl-by-example
 
The PDF document can be directly accessed through
 
            https://github.com/fraunhoferfokus/acsl-by-example/blob/master/ACSL-by-Example.pdf
 
This is a minor release where we among other things
 
	- Slightly change the definition of predicate HasEqualNeighbors and its use in the specification of ,adjacent_find;. 
	- Remove the algorithm ‚remove' and the more elaborate version of ‚remove_copy'. 
	  We are currently working on new specifications of these algorithms. 
	- Adapt some Coq proofs related to the logic function Count in order to reflect changes in output of Frama-C/WP.
	- Remove table on ACSL lemmas that had to be proved by Coq.
 
We hope this document helps you in your work with Frama-C/WP.
 
Regards
 
Jens Gerlach