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] Res: Jessie global variables and functions

Jo?o Paulo Carvalho wrote:
> > A correct specification for f2 as it is written would be assigns 
> var1, var2;
>
> So you always need to manually propagate the assigns clause of every 
> function which is called by the function in focus?
>
> Is this correct?
>
> If yes, does you agree that it would be the case to implement in Why 
> some kind of automatically propagation of the refered (indirectly) 
> assigns clauses?
>
Certainly not the Jessie/Why job. But as I said in a recent mail, 
another plugin dedicated to suggesting simple annotations could be useful.

I also repeat that I think it would be a bad idea if generated 
annotations would be hidden from the user.

Also, notice that generating accurate assigns clauses (or requires or 
ensures) is a difficult problem. See Pascal's answer.

For more information, you can look and Y Moy's Phd thesis for complex 
techniques for generating annotations :

http://www.lri.fr/~marche/moy09phd.pdf

These are implemented in Jessie, but still in a very experimental stage 
to my point of view. Please fell free to experiment with it (you need to 
install the APRON library when you compile Why). Also, unfortunately, 
generated annotations are not given back into the C source.

- Claude

> Att.
> Jo?o Paulo Carvalho.
>
>
> ------------------------------------------------------------------------
> Veja quais s?o os assuntos do momento no Yahoo! + Buscados: Top 10 
> <http://br.rd.yahoo.com/mail/taglines/mail/*http://br.maisbuscados.yahoo.com/> 
> - Celebridades 
> <http://br.rd.yahoo.com/mail/taglines/mail/*http://br.maisbuscados.yahoo.com/celebridades/> 
> - M?sica 
> <http://br.rd.yahoo.com/mail/taglines/mail/*http://br.maisbuscados.yahoo.com/m%C3%BAsica/> 
> - Esportes 
> <http://br.rd.yahoo.com/mail/taglines/mail/*http://br.maisbuscados.yahoo.com/esportes/> 
>
> ------------------------------------------------------------------------
>
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at 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                    |