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] [ACSL] proposition finale comme définition de "allocates"

  • Subject: [Frama-c-discuss] [ACSL] proposition finale comme définition de "allocates"
  • From: Patrick.Baudin at cea.fr (BAUDIN Patrick)
  • Date: Thu, 16 Feb 2012 11:40:40 +0100
Bonjour ? tous,

Lors de notre derni?re r?union ACSL, nous avons parl? d'avoir une clause 
\allocated{L}(p)
qui retourne \true si et seulement si la zone m?moire point?e par p est 
allou?e dynamiquement.

Pourquoi pas, mais j'aimerais bien aussi une fonction \alloc telle que
pour tout pointeur p \alloc{L}:(p) \in { \dynamic, \auto, \static, 
\register, \unallocated }
avec \allocated{L}(p) ?quivalent ? \alloc{L}(p)==\dynamic.

Cette fonction \alloc serait utilis?e dans la d?finition de la clause 
allocates.

Rappel, en C "auto" signifie "dans la pile", et
"register" signifie "dans un registre ou dans la pile, mais en tout cas, 
on ne peut pas en prendre l'adresse".
Ce dernier point "dont on ne peut pas en prendre l'adresse" avait ?tait 
abord? en r?union par Pascal au
sujet des champs de bits. C'est un premier vers ce besoin.

Cela vous convient'il comme premi?re proposition : avoir une fonction 
\alloc retournant le mode d'allocation ?

Ensuite, je vous rappelle la d?finition donn?e ? la clause "allocates" :
La clause "allocates P1,...Pn;" est ?quivalente ? une post-condition du 
genre :

\forall char* p; \separated(p,\union(P1,...,Pn))
==> (\base_addr{Post}(p) == \base_addr{Pre}(p) &&
      \block_length{Post}(p) == \block_length{Pre}(p)
      \valid{Post}(p) == \valid{Pre}(p))

Cela me semble insuffisant. Il y a en plus du \valid, le \valid_read qui 
ne change pas,
tout comme le mode d'allocation.

Voici une nouvelle d?finition pour la clause "allocates P1,...Pn;"
\forall char* p; \separated(p,\union(P1,...,Pn))
==> (\base_addr{Post}(p) == \base_addr{Pre}(p) &&
      \block_length{Post}(p) == \block_length{Pre}(p)
      \valid{Post}(p) == \valid{Pre}(p) &&
      \valid_read{Post}(p) == \valid_read{Pre}(p) &&
      \alloc{Post}(p) == \alloc{Pre}(p) )

Etes-vous d'accord avec cette nouvelle proposition ?

Patrick.

-- 

Patrick Baudin, DILS/LSL, B?t. 862,
Point Courrier n? 174
Institut CARNOT CEA LIST,
CEA Saclay Nano-INNOV,
91191 Gif-sur-Yvette cedex, France.
tel: +33 (0)1 6908 2072