--- layout: fc_discuss_archives title: Message 2 from Frama-C-discuss on April 2008 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Re: Pb sur Caduceus1.10b/Why v2.10b



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