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: Patrick.Baudin at cea.fr (BAUDIN Patrick)
  • Date: Mon Apr 21 15:13:20 2008
  • In-reply-to: <480C88AE.7040106@inria.fr>
  • References: <A6FD74D4A6DA4247AD801E394363406302B138D2@sctex002.st-cloud.dassault-avion.fr> <480C88AE.7040106@inria.fr>
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
>>  
>>  
>