--- layout: fc_discuss_archives title: Message 80 from Frama-C-discuss on February 2012 ---
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>