--- layout: fc_discuss_archives title: Message 1 from Frama-C-discuss on April 2008 ---
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 |