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] Re: Pb sur Caduceus1.10b/Why v2.10b

  • Subject: [Frama-c-discuss] Re: Pb sur Caduceus1.10b/Why v2.10b
  • From: Claude.Marche at inria.fr (Claude Marché)
  • Date: Mon Apr 21 14:31:28 2008
  • In-reply-to: <A6FD74D4A6DA4247AD801E394363406302B138D2@sctex002.st-cloud.dassault-avion.fr>
  • References: <A6FD74D4A6DA4247AD801E394363406302B138D2@sctex002.st-cloud.dassault-avion.fr>
Bonjour Dillon,

Je me permets de repondre avec copie aux developpeurs de Frama-C, car 
cela les concerne.

En fait, je ne comprends pas quand tu dis que ca marchait dans une 
ancienne version de Caduceus. A mon avis ca n'a jamais march?, ou alors 
c'etait un bug avant.

Le pb est plutot une insuffisance dans l'expressivite du langage de 
spec. Dans ACSL, le pb se pose egalement.

Est-ce qu'il y a une solution dans Caveat ?

- Claude

Pariente Dillon wrote:
> Bonjour ? vous deux,
>  
> Ce qui ressemble ? un bug est apparu sur le petit exemple suivant :
> 
>     typedef struct { int a; } las;
>     las * p;
>      
>     /*@
>     requires \valid(p)
>     assigns p->a
>     */
>     void f()
>     { p->a = 5; }
>      
>     /*@
>     assigns p->a
>     */
>     void g(int * p)
>     { f(); }
> 
> La spec de g() est refus?e par Caduceus, qui consid?re - ? juste titre - 
> que p (pris comme param?tre formel de g) n'est pas un pointeur de structure.
> Mais alors, comment faire r?f?rence ? p "pointeur global" affect? dans 
> f, dans la spec de g ?
>  
> Du coup, je commence ? comprendre pourquoi Benjamin, dans Frama-C, 
> renomme les param?tres formels dont le nom est d?j? d?clar? en global !
> (ce qui me pose quelques soucis dans le d?veloppement de Gena sous 
> Frama-C !)
>  
> Par avance, merci de me donner votre avis sur ce point, et bonne nourn?e !
>  
>   Cordialement,
>   Dillon Pariente
>  
>   -----
>   Dillon.Pariente@dassault-aviation.fr 
> <mailto:Dillon.Pariente@dassault-aviation.fr>
>   Dassault Aviation - DGT/DPR
>   78, quai Marcel Dassault - F-92552 Saint-Cloud Cedex 300
>   Phone: +33 (0)1.47.11.46.68 - Fax: +33 (0)1.47.11.53.65
>  
>  

-- 
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                    |