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 for Frama-C Boron

  • Subject: [Frama-c-discuss] ACSL by Example for Frama-C Boron
  • From: jens.gerlach at first.fraunhofer.de (Jens Gerlach)
  • Date: Wed, 26 May 2010 15:31:11 +0200
The DEVICE-SOFT team at Fraunhofer FIRST is pleased to announce the  
availability of

	"ACSL by Example"  version 5.1.0.

The tutorial, which corresponds to Frama-C Boron, can be downloaded  
directly through the following link

	http://www.first.fraunhofer.de/owx_download/acsl-by-example-5_1_0.pdf

For more information on the DEVICE-SOFT project please refer to our  
project page

	http://www.first.fraunhofer.de/device_soft_en


Here is a list of changes since version 4.2.1

- adaption to Frama-C Boron and Why 2.26 releases
- changed from the -jessie-no-regions command-line option to using the  
pragma SeparationPolicy(value)

- changed to latest version of CVC3 2.2
- added additional remarks to our implementation of find first of  
(Section 3.5)
- changed size_type (int) to integer in all speci?cations
- removed casts in fill and iota
- renamed is_valid_range as IsValidRange
- renamed has_value as HasValue
- renamed predicate all_equal as IsEqual
- extended timeout to 30 sec.


Regards,

Jens Gerlach





-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20100526/4fd6ae1b/attachment-0001.htm>