--- layout: fc_discuss_archives title: Message 37 from Frama-C-discuss on September 2009 ---
Voici un exemple de code repr?sentatif pour ?tayer la discussion: int exit (int status) ; extern int calls_tab[], calls_cpt ; #define EXIT_CALL_ID 33 void ASRT_ASSERT (int cond) { if (! cond) { calls_tab[calls_cpt] = EXIT_CALL_ID ; ++calls_cpt ; exit (2) ; } } extern int tab_panne [] ; int find (int min, int panne, int pos_depart) { int ret=0; int indice = pos_depart; ASRT_ASSERT(min<=pos_depart); while (indice!=min && ret==0) { indice--; if (tab_panne[indice]==panne) ret =-1; } return ret; } Selon ma proposition, une sp?cification de ce code pourrait ?tre : /*@ 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); /*@ terminates \true ; @ requires \true ; @ behavior continues : // Cas sans exit(); @ assumes cond != 0 ; @ assigns \nothing ; @ exits \false ; @ behavior exits : // Cas sans return(); @ assumes cond == 0; @ requires \valid(&calls_tab[calls_cpt]) ; @ ensures \false ; @ exits \result == 2 && calls_cpt == \old(calls_cpt) + 1 && @ calls_tab[calls_cpt] == 33 ; @ exit_assigns calls_tab[calls_cpt] ; @ complete continues, exits; // aspect compl?tude @ disjoint continues, exits; // et exclusivit? des cas. @*/ void ASRT_ASSERT(int cond); /*@ terminates \true ; @ requires \true ; @ behavior not_found : @ assumes (min<=pos_depart) && \forall int k ; ... @ requires \valid ... @ ensures \result == 0 @ assigns \nothing ; @ exits \false ; @ behavior found : @ assumes (min<=pos_depart) && \exists int k ; ... @ requires \valid ... @ ensures \result == 1 ; @ assigns \nothing ; @ exits \false ; @ behavior exits : @ assumes !(min<=pos_depart); @ requires \valid(&calls_tab[calls_cpt]) ; @ ensures \false ; @ exits \result == 2 && calls_cpt == \old(calls_cpt) + 1 && @ calls_tab[calls_cpt] == 33 ; @ exit_assigns calls_tab[calls_cpt] ; @ complete found, not_found, exits; @ disjoint found, exits; @ disjoint not_found, exits; @ disjoint found, not_found; @*/ int find (int min, int panne, int pos_depart) ; -- Patrick Baudin, CEA, LIST, SOL, F-91191 Gif-sur-Yvette cedex, France. tel: +33 (0)1 6908 2072