--- layout: fc_discuss_archives title: Message 37 from Frama-C-discuss on September 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] exit_behavior pour la prochaine réunion



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