--- layout: fc_discuss_archives title: Message 80 from Frama-C-discuss on February 2012 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Fwd: [ACSL] proposition finale comme définition de "allocates"



Sorry for the error of the recipient.

-------- Message original --------
Sujet: 	[Frama-c-discuss] [ACSL] proposition finale comme d?finition de 
"allocates"
Date : 	Thu, 16 Feb 2012 11:40:40 +0100
De : 	BAUDIN Patrick <Patrick.Baudin at cea.fr>
R?pondre ? : 	Frama-C public discussion 
<frama-c-discuss at lists.gforge.inria.fr>
Pour : 	Frama-C public discussion <frama-c-discuss at lists.gforge.inria.fr>



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


_______________________________________________
Frama-c-discuss mailing list
Frama-c-discuss at lists.gforge.inria.fr
http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss
.


-------------- section suivante --------------
Une pi?ce jointe HTML a ?t? nettoy?e...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20120216/66ebc13d/attachment-0001.htm>