Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

  • Subject: [Frama-c-discuss] exit_behavior pour la prochaine réunion
  • From: Patrick.Baudin at cea.fr (BAUDIN Patrick)
  • Date: Tue, 15 Sep 2009 13:08:08 +0200
  • In-reply-to: <4AAE5087.1010509@cea.fr>
  • References: <4AAE5087.1010509@cea.fr>
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