--- layout: fc_discuss_archives title: Message 102 from Frama-C-discuss on December 2009 ---
[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                    |