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]

RE  : [Frama-c-discuss] YASE \lambda

Thanks. I see that the non-implemented features are signaled by being 
underlined and with a grey line in the margin. However, the version of 
this same document downloadable on http://frama-c.cea.fr/acsl.html, and 
which I had looked at before, does not provide such information; it's 
almost the same document, either an earlier version or a forked version, 
but with exactly the same title and and date. Maybe it would be good to 
synchronize the two documents.
Also, is it right that the marked features correspond to version Helium? 
Which such marked features will be unmarked with the Lithium version?
Thanks,
Jean-Baptiste Jeannin





"MONATE Benjamin 205998" <Benjamin.MONATE@cea.fr> 
20/10/2008 11:44

A
<jean-baptiste.jeannin@hispano-suiza-sa.com>, 
<frama-c-discuss@lists.gforge.inria.fr>
cc

Objet
RE : [Frama-c-discuss] YASE \lambda






Hi,

As for general Frama-C support refer to the document 
"doc/acsl-implementation.pdf".
As for Jessie, something will be provided with the next release.

Hope this helps,
Benjamin Monate



-------- Message d'origine--------
De: frama-c-discuss-bounces@lists.gforge.inria.fr de la part de 
jean-baptiste.jeannin@hispano-suiza-sa.com
Date: lun. 20/10/2008 11:24
?: frama-c-discuss@lists.gforge.inria.fr
Objet : Re: [Frama-c-discuss] YASE \lambda
 
More generally, is there a simple way to know, both for the Helium and the 

Lithium release, what part of ACSL is implemented? More generally, it 
would be good to know:
- the exact subset of ACSL supported by each release.
- the exact subset of ACSL supported by the Jessie plugin of each release.

Is this documented somewhere? I thought I had understood that the 
non-implemented features were marked as so in the ACSL doucmentation, but 
now I cannot find how.

Thanks,
Jean-Baptiste Jeannin




Claude March? <Claude.Marche@inria.fr> 
Envoy? par : frama-c-discuss-bounces@lists.gforge.inria.fr
17/10/2008 14:35

A
Christoph Weber <Christoph.Weber@first.fraunhofer.de>
cc
frama-c-discuss@lists.gforge.inria.fr
Objet
Re: [Frama-c-discuss] YASE \lambda








Unfortunately, this feature is not expected to be available in the next 
release. Indeed neither \lambda nor \sum. The only thing we can propose 
is a work-around, for providing an ad-hoc (e.g specific for each 
example) equivalent specification.

- Claude

Christoph Weber wrote:
> Salut,
> 
> I'm thinking about some stuff I found in the acsl1_3 manual. I 
encountered \lambda, it seems comfortable so I wonder will following 
example work in the next release?
> 
> /*@
>  requires last > first;
>  requires \valid_range(first, 0, last-first -1);
>  ensures  \result == \sum(0, last-first -1,(\lambda integer k ; first[k] 

== value ? 1 : 0)); 
> 
> */
> int count_int_array ( int* first, int* last, int value )
> {
>   int ret=0;
>   //@ ghost int* a = first;
>     /*@
>      loop invariant a <= first <= last;
>      loop invariant ret == \sum(0, first-a-1,(\lambda integer k ; 
first[k] == value ? 1 : 0));
>     */
>   while (first != last) if (*first++ == value) ++ret;
>   return ret;
> }
> 
> Merci d'avance
> 
> Christoph
> 
> 
> 
> ------------------------------------------------------------------------
> 
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss@lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss

-- 
Claude March?                          | tel: +33 1 72 92 59 69
INRIA Saclay - ?le-de-France           | mobile: +33 6 33 14 57 93
Parc Orsay Universit?                  | fax: +33 1 74 85 42 29
4, rue Jacques Monod - B?timent N      | http://www.lri.fr/~marche/
F-91893 ORSAY Cedex                    |







_______________________________________________
Frama-c-discuss mailing list
Frama-c-discuss@lists.gforge.inria.fr
http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss


#
" This e-mail and any attached documents may contain confidential or 
proprietary information. If you are not the intended recipient, please 
advise the sender immediately and delete this e-mail and all attached 
documents from your computer system. Any unauthorised disclosure, 
distribution or copying hereof is prohibited."

 " Ce courriel et les documents qui y sont attaches peuvent contenir des 
informations confidentielles. Si vous n'etes  pas le destinataire 
escompte, merci d'en informer l'expediteur immediatement et de detruire ce 
courriel  ainsi que tous les documents attaches de votre systeme 
informatique. Toute divulgation, distribution ou copie du present courriel 
et des documents attaches sans autorisation prealable de son emetteur est 
interdite."
#



#
" This e-mail and any attached documents may contain confidential or proprietary information. If you are not the intended recipient, please advise the sender immediately and delete this e-mail and all attached documents from your computer system. Any unauthorised disclosure, distribution or copying hereof is prohibited."

 " Ce courriel et les documents qui y sont attaches peuvent contenir des informations confidentielles. Si vous n'etes  pas le destinataire escompte, merci d'en informer l'expediteur immediatement et de detruire ce courriel  ainsi que tous les documents attaches de votre systeme informatique. Toute divulgation, distribution ou copie du present courriel et des documents attaches sans autorisation prealable de son emetteur est interdite."
#
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20081020/7e469f43/attachment.html