Assertion sur pointeur sur un tableau

Question

J'ai défini la fonction suivante qui est bien prouvé par Frama-c:

//ensures array <= \result < array+length && *\result == element; 
/*@ 
    requires 0 < length; 
    requires \valid_read(array + (0 .. length-1)); 

    assigns \nothing; 

    behavior in: 
    assumes \exists int off ; 0 <= off < length && array[off] == element; 
    ensures *\result == element; 

    behavior notin: 
    assumes \forall int off ; 0 <= off < length ==> array[off] != element; 
    ensures \result == 0; 

    disjoint behaviors; 
    complete behaviors; 
*/ 
int* search(int* array, int length, int element){ 
    int *tmp; 
    /*@ 
    loop invariant 0 <= i <= length; 
    loop invariant \forall int j; 0 <= j < i ==> array[j] != element; 
    loop assigns i; 
    loop variant length-i; 
    */ 
    for(int i = 0; i < length; i++) 
    { 
    if(array[i] == element) 
    { 
     tmp = &array[i]; 
     //@ assert *tmp==element; 
    } 
    else 
    { 
     tmp = 0;  
    } 
    } 
    return tmp; 
} 

et je l'utilise dans la principale entrée suivante:

int main(){ 
    int arr[5]={1,2,3,4,5}; 
    int *p_arr; 

    p_arr = search(arr,5,4); 
    //@ assert *p_arr==30; 

    return 0 
} 

Je me demande pourquoi frama-c donne l'assertion "// @ assert * p_arr == 30;" comme vrai, je ne comprends pas.

Merci

Answer 1

Utilisation de la ligne de commande uniquement, j'ai vu quelques problèmes dans votre code:

• tmp est manquant dans la boucle affecte;
• vous devez:
  • soit ajouter une break dans la branche then de la fonction seach (alors vous retourner le pointeur sur le premier élément correspondant)
  • ou initialiser tmp = 0 au début de la fonction et supprime la branche else dans la boucle (alors vous retourneriez un pointeur sur la dernière occurrence).

Je n'ai pas essayé l'interface graphique, mais il semble étrange que vous dites que votre exemple est:

bien prouvé par Frama-c

Je suggère que vous utilisez la ligne de commande pour commencer.

Answer 2

Ok maintenant je corriger mon code comme suit:

//ensures array <= \result < array+length && *\result == element; 
/*@ 
    requires 0 < length; 
    requires \valid_read(array + (0 .. length-1)); 

    assigns \nothing; 

    behavior in: 
    assumes \exists int off ; 0 <= off < length && array[off] == element; 
    ensures *\result == element; 

    behavior notin: 
    assumes \forall int off ; 0 <= off < length ==> array[off] != element; 
    ensures \result == 0; 

    disjoint behaviors; 
    complete behaviors; 
*/ 
int* search(int* array, int length, int element){ 

    /*@ 
    loop invariant 0 <= i <= length; 
    loop invariant \forall int j; 0 <= j < i ==> array[j] != element; 
    loop assigns i; 
    loop variant length-i; 
    */ 
    for(int i = 0; i < length ; i++) 
    { 
    if(array[i] == element) 
    { 
     return &array[i]; 
    } 
    } 
    return 0; 
} 

et ajoutez l'affirmation suivante:

int main() 
{ 
    int arr[5] = {1,2,3,4,5}; 
    int *ptr; 

    ptr = search(arr,5,3); 
    //@ assert *ptr==3; 

} 

puis exécutez: Frama-c -wp -rte myfile.c et a obtenu le résultat :

[wp] Proved goals: 65/65 
    Qed:   35 (1.00ms-6ms-24ms) 
    Alt-Ergo:  30 (16ms-30ms-94ms) (132) 

Si je mets une autre affirmation:

int main() 
    { 
     int arr[5] = {1,2,3,4,5}; 
     int *ptr; 

     ptr = search(arr,5,3); 
     //@ assert *ptr==5; 

    } 

Puis-je obtenir la sortie:

[wp] [Alt-Ergo] Goal typed_main_assert_2 : Timeout (Qed:4ms) (10s) 
[wp] Proved goals: 64/65 
    Qed:   35 (1.00ms-4ms-10ms) 
    Alt-Ergo:  29 (16ms-28ms-109ms) (132) (interrupted: 1) 

Donc, l'affirmation est « inconnu » comme nous l'espérions et si nous courons Frama-c-la balle est gui orange.

Alors ça marche très bien, attention aux mauvaises choses axiomatiques! Merci Anne pour votre aide.