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