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

  • Subject: [Frama-c-discuss] Fwd: [ACSL] proposition finale comme définition de "allocates"
  • From: Patrick.Baudin at cea.fr (BAUDIN Patrick)
  • Date: Thu, 16 Feb 2012 15:36:45 +0100
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>