--- layout: fc_discuss_archives title: Message 36 from Frama-C-discuss on September 2009 ---
Le cas de la terminaison par un appel ? la fonction exit() s'apparente aux terminaisons abruptes des contrats d'instruction (clauses "breaks", "continues" et "returns"). Il serait possible d'y ajouter une clause "exits" o? "\result" d?signe la valeur pass?e en argument ? la fonction exit(). Par contre, cette clause "exits" serait d'autoris?e dans les contrats de fonction. Afin que ces clauses puissent ?tre sous le coup d'un "assumes", il faudrait les autoriser en tant que clauses de "simple-behavior" et de "named-behavior". Cela autorise d'?tudier le caract?re "disjoint" et "complete" des sp?cifications qui est un point largement utilis? par Airbus. Il n'est donc pas n?cessaire d'avoir un mot cl? diff?rent de "behavior" comme cela est propos? dans la version courante d'ACSL. Le seul besoin est de popuvoir sp?cifier les locations modifi?s lors des chemins d'ex?cution menant ? une termaison abrupte. Je propose l'ajout des clauses suivantes aux clauses abruptes : "break_assigns", "continue_assign", "returns_assigns" et "exit_assigns". Voici les sp?cifications de la fonction exit : /*@ terminates T:\true ; // Elle ne boucle jamais ind?finiment, @ requires \true ; // et ne requiert rien de particulier. @ behavior always_exits : @ assumes \true ; // Dans tous les cas, @ requires \true ; // sans ne rien requ?rir d'autre, @ ensures E:\false ; // elle n'effectue aucun "return" et @ // lorsque la fonction sort en "exit" (il @ // en est toujours ainsi vu les clauses @ exits \result == status ;// T et E) c'est avec la valeur "status" @ exits_assigns \nothing ; // sans modifier aucune variable. @*/ int exit(int status); Voici les sp?cifications d'une fonction assert : /*@ terminates \true ; @ requires \true ; @ behavior continues : // Cas sans exit(); @ assumes cond != 0 ; @ assigns \nothing ; @ exits \false ; @ behavior exits : // Cas sans return(); @ assumes cond == 0; @ ensures \false ; @ exits \result == 1 @ exit_assigns \nothing ; @ complete continues, exits; // aspect completude @ disjoint continues, exits; // et exclusivite des cas. @*/ void assert(int cond); Que pensez-vous cette proposition ? -- Patrick Baudin, CEA, LIST, SOL, F-91191 Gif-sur-Yvette cedex, France. tel: +33 (0)1 6908 2072