Compréhension des étiquettes logiques de Frama-C

Question

J'ai quelques problèmes lorsque j'essaie d'utiliser les étiquettes logiques par défaut LoopEntry et LoopCurrent. Voici un exemple simple que les différents prouveurs (alt-ergo, coq, cvc3, z3) que j'utilise ne parviennent pas à prouver :

/*@ requires n > 0;*/
void f(int n){
    int i = 0;
    /*@ loop invariant \at(i,LoopEntry) == 0;
      @ loop invariant \at(i,LoopCurrent) >= \at(i,LoopEntry);
      @ loop invariant 0 <= i <= n;
      @ loop assigns i;
      @ loop variant n-i;
    */
    while(i < n){
        i++;
    }
}

En particulier, les première et deuxième invariants ne sont pas prouvés (pas de problème avec les autres). Maintenant, si je modifie cet exemple simple en ajoutant une étiquette "label" après la déclaration/définition de i et si je me réfère à cette étiquette, et change LoopCurrent par Ici (ce qui donne ce extrait :

/*@ requires n > 0;*/
void f(int n){
    int i = 0;
    label : ;
    /*@ loop assigns i;
      @ loop invariant \at(i,label) == 0;
      @ loop invariant \at(i,Here) >= \at(i,label);
      @ loop invariant 0 <= i <= n;
      @ loop variant n-i;
    */
    while(i < n){
        i++;
    }
}

)

maintenant tout est prouvé.

J'ai trouvé la documentation sur les étiquettes logiques par défaut d'Acsl assez facile à comprendre et je m'attendais à ce que le premier exemple soit prouvé comme le second. Pourriez-vous expliquer d'où vient le problème ?

Roo

PS1 : à quoi se réfère Pre lorsqu'il est utilisé dans une clause de boucle ? L'état avant la première itération de la boucle ou l'itération précédente ?

PS2 : J'utilise Frama-C Fluorine, mais peut-être que je n'ai pas mis à jour pour chaque mise à jour mineure

Answer 1

LoopCurrent et LoopEntry ne sont en effet pas pris en charge par WP dans Fluorine. Cela a été corrigé dans la version de développement (voir http://bts.frama-c.com/view.php?id=1353), et devrait apparaître dans la prochaine version.

En ce qui concerne les autres étiquettes prédéfinies,

• Pre fait toujours référence à l'état au début de la fonction.
• Old ne peut être utilisé que dans un contrat, et fait référence à l'état préalable de ce contrat (c'est-à-dire l'état dans lequel les clauses requires et assumes sont évaluées). Il est donc équivalent à Pre pour un contrat de fonction, mais pas pour un contrat de statement (à moins que vous ne fassiez un contrat incluant le bloc principal de votre fonction).
• Here signifie le point du programme où l'annotation correspondante est évaluée. Dans un contrat, sa signification dépend de la clause dans laquelle elle apparaît.
• Post ne peut être utilisé que dans les clauses ensures, assigns, allocates ou frees, et fait référence à l'état à la fin du contrat.