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] Frama-c wiki and New version of ACSl by Example

  • Subject: [Frama-c-discuss] Frama-c wiki and New version of ACSl by Example
  • From: Patrick.Baudin at (BAUDIN Patrick)
  • Date: Wed, 01 Oct 2014 11:40:41 +0200
  • In-reply-to: <>
  • References: <>

Dear Jens,

I wanted to update the Frama-C wiki which already refers your document.
Good, the link is unchanged.

But, when updating the version number given into that wiki, I saw an 
eventual problem with your document.
In section A.1 about changes, it is written that this new version is 
"not yet published" !

So, are we allowed to have a such link to your document from our wiki?


Le 30/09/2014 16:13, Gerlach, Jens a ?crit :
> Dear Frama-C Users,
> Fraunhofer FOKUS has just provided an updated version of  ?ACSL by Example?.
> The new version is accessible through
> It works with Frama-C Neon and includes the following changes
> 	? remove additional labels in the assumes clauses of some stack function that were necessary due to an error in Oxygen
> 	? provide a second version of remove_copy (see Sections 6.9 and 6.10) in order to explain the specification of the stability of the algorithms
> 	? coarsen loop assigns of mutating algorithms
> 	? temporarily remove the unique_copy algorithm
> Regards
> Jens Gerlach
> Head of Verification Group
> Fraunhofer FOKUS
> Berlin, Germany
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at

Patrick Baudin, DILS/LSL, B?t. 862,
Point Courrier n? 174
CEA Saclay Nano-INNOV,
91191 Gif-sur-Yvette cedex, France.
tel: +33 (0)1 6908 2072