--- layout: fc_discuss_archives title: Message 36 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



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