--- layout: fc_discuss_archives title: Message 2 from Frama-C-discuss on April 2008 ---
Bonjour A la question suivante : > Est-ce qu'il y a une solution dans Caveat ? Oui, il y a une solution CAVEAT ? ce probl?me de nommage. Elle n'avait pas ?t? retenue lors de nos premi?res r?unions ACSL. La principale raison ?tait qu'ACSL se voulait ?tre un langage de sp?cification pour une v?rification a priori et non a postiori. Le code se doit de r?pondre ? une notion de testabilit? sp?cifique ? la preuve. Cette notion est pr?sente dans JML, o? l'on ne peut que parler que de ce qui est accessible. Dans ACSL, la notion de ghost vise ? relativiser notre position. Elle permet de rendre accessibles les choses qui ne le sont pas. C'est ainsi que l'on peut faire de la v?rification a postiori. Ici, on pourrait introduire une variable ghost ainsi: typedef struct { int a; } las; las * p; //@ghost las ** const PP=&p; typedef struct { int a; } las; las * p; /*@ requires \valid(p) assigns p->a */ void f() { *PP->a = 5; } /*@ assigns *PP->a */ void g(int * p) { f(); } Cordialement, Patrick. -- Patrick Baudin, CEA LIST tel: +33 (0)1 6908 2072 > > 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 >> >> >