Frama-C-discuss mailing list archives

Romain.Jobredeaux at supelec.fr (Romain Jobredeaux) · Mon, 04 Oct 2010 23:18:25 +0200

Hi,

Sorry I didn't realize this list was english-only.

Thank you for the quick reply. I followed your advice, I 'lightened'  
the annotations a bit, everything goes through except for 2 proofs  
that are directly related with the 'assigns' clauses in the function  
'ones'. I'm attaching the other function this time (allocM function  
included):

/*@
   @ requires m > 0 && n >0 ;
   @ assigns \nothing;
   @ ensures (\valid(\result + (0..m-1)) && (\forall integer  k; 0 <=  
k < m ==> \valid(\result[k] +(0..n-1) ) ) );
*/

float** allocM (int m,int n)
{
	int  i = 0;
	float** p;
	p= malloc(m *sizeof(float *));

         /*@ assert \valid_range(p,0,m-1); */

         /*@ assert p != \null; */
	/*@ loop assigns p[0..m-1];
           @ loop invariant (0 <= i <= m) &&  (\forall integer k;  (0  
<= k < i ) ==> \valid(p[k] + (0..n-1)) );
           @ loop variant  m-i;
	  @ */
	for (i = 0; i<m;i++)
	{
                 /*@ assert 0 <= i < m; */
		(p)[i] = malloc(n * sizeof(float));
		/*@ assert \valid(p[i] +(0..n-1)); */

	}
	return p;
}

/*@ requires m > 0 && n > 0;
   @
   @ assigns \nothing;
   @ ensures  \result == \null || (\forall integer i; \forall integer j;
   @       0 <= i < m && 0 <= j <n ==> *(\result[i]+j)  == 1.0);
*/

float** ones(int m,int n)
{
     /*@ assert m > 0  && n > 0; */

     float **c = allocM(m,n);

     /*@ assert (\valid(c+ (0..m-1)) && (\forall integer  k; 0 <= k <  
m ==> \valid(c[k] +(0..n-1) ) )) ; */

     int i = 0;
     int j = 0;

     /*@  loop assigns *(c[0..m-1] + (0..n-1));
       @ loop invariant  (0 <= i <=m) && (\forall integer k; \forall  
integer q;  (0<= k < i && 0 <= q < n) ==> (*(c[k]+q) == 1.0)) ;
       @  loop variant m-i ;
       */
     for (i = 0; i<m; i++){
     /*@ assert 0<= i < m; */
     /*@ assert \valid(c[i]+(0..n-1)); */

     /*@ loop assigns  *(c[i] +(0..n-1));
       @ loop invariant (0 <= j <= n) && (\forall integer l; 0 <= l <  
j ==> ( *(c[i] + l)  == 1.0) );
       @ loop variant n-j ;
       */
         for (j = 0; j<n;j++){

         /*@ assert  0<=j < n ; */
         /*@ assert \valid(c[i]+j); */
	  *(c[i] + j) = (float) 1.0;
         }
     }
     return c;
}

the outer loop 'assigns' clause and the one for the function as a  
whole generate proof obligations that are not handled by any of the  
provers. The clause in the inner loop is handled. I don't understand  
why.

Thanks in advance,

Romain.

Quoting Claude Marche <Claude.Marche at inria.fr>:

> Hi,
>
> First of all, please note that it is an english speaking list, do  
> not send messages in french please.
>
> A few remarks first:
>
> * replace each "\forall int" by "\forall integer" and remove each  
> cast "(float)" in specifications, it will avoid
>   unnecessary extras casts hence might make prover's life easier
>
> * your file is not self-contained: NULL undefined, allocM  
> undeclared. replacing NULL by \null helps.
>
> * the spec of allocM is crucial for your problems with assigns  
> clauses since if you expect it to allocate a new block,
>   you have to specify that.
>
> * for me, using provers Alt-Ergo, Simplify, Z3 and CVC3, everything  
> is proved except the VC corresponding
>   to your main "assigns \nothing" clause. Which is not correct if  
> allocM is not specified correctly.
>
>   Try to install more provers if needed: see  
> http://why.lri.fr/provers.en.html
>
>   In particular the preservation of your loop invariants seems to be OK
>
> Hope this helps,
>
> - Claude
>
> On 09/24/2010 06:04 PM, Romain Jobredeaux wrote:
>> Bonjour,
>>
>> Ce message fait suites aux questions d'Alwyn Goodloe de d?but  
>> juillet sur les boucles imbriqu?es et les tableaux ? dimensions  
>> multiples (qui comme on l'a fait remarquer pr?c?demment n'en sont  
>> pas vraiment, puisqu'il s'agit en fait de pointeurs doubles  
>> pointant sur un tableau de pointeurs). La fonction d'allocation  
>> passe maintenant toutes les obligations de preuves, mais nous  
>> rencontrons encore des difficult?s avec la fonction suivante, qui  
>> alloue une "matrice" de taille m,n et la remplit de 1 :
>>
>> /*@ requires m > 0 && n > 0;
>>  @  assigns \nothing;
>>  @
>>  @  ensures  \result == NULL || (\forall int i; \forall int j;
>>  @       0 <= i < m && 0 <= j <n ==> *(\result[i]+j)  == (float) 1.0);
>> @*/
>>
>> float** ones(int m,int n)
>> {
>>    /*@ assert m > 0 && n > 0; */
>>
>>    float **c = allocM(m,n);
>>
>>    /*@ assert (\valid(c+ (0..m-1)) && (\forall int  k; 0 <= k < m  
>> ==> \valid(c[k] +(0..n-1) ) )) ; */
>>
>>    int i = 0;
>>    int j = 0;
>>
>>
>>    /*@  loop assigns *(c[0..m-1]+(0..n-1));
>>      @ loop invariant  (0 <= i <=m) && (\forall int k; \forall int  
>> q;  (0<= k < i && 0 <= q < n) ==> (*(c[k]+q) == (float) 1.0)) ;
>>      @  loop variant m-i ;
>>      */
>>    for (i = 0; i<m; i++){
>>    /*@ assert 0<= i < m; */
>>    /*@ assert \valid(c[i]+(0..n-1)); */
>>
>>    /*@ loop assigns  *(c[i] +(0..n-1));
>>      @ loop invariant (0 <= j <= n) && (\forall int l; 0 <= l < j  
>> ==> ( *(c[i] + l)  == (float)1.0) );
>>      @ loop invariant \forall int p; \forall int q;  (0 <= p <i &&  
>> 0 <= q < n) ==> *(c[p]+q) == \at(*(c[p]+q),Here) ;
>>      @ loop invariant \forall int p; \forall int q;  (i < p <n && 0  
>> <= q < n) ==> *(c[p]+q) == \at(*(c[p]+q),Here) ;
>>      @ loop variant n-j ;
>>      */
>>        for (j = 0; j<n;j++){
>>
>>        /*@ assert  0<=j < n ; */
>>        /*@ assert \valid(c[i]+j); */
>>      *(c[i] + j) = (float) 1.0;
>>       /*@ assert *(c[i] + j) == (float) 1.0; */
>>        }
>>    /*@ assert \forall int l; 0 <= l < n ==> ( *(c[i] + l)  ==  
>> (float)1.0) ; */
>>
>>
>>    }
>>    return c;
>> }
>> Seules 3 obligations de preuves ne sont pas prouvees  
>> automatiquement (parmi les 38 de default behavior), et notamment  
>> l'invariant de boucle exterieure (qui est en fait le plus important  
>> pour nous) :
>> /*@ loop invariant  (0 <= i <=m) && (\forall int k; \forall int q;   
>> (0<= k < i && 0 <= q < n) ==> (*(c[k]+q) == (float) 1.0))
>>
>> Les deux autre invariants non prouv?s concernent des conditions de  
>> type "not_assigns" sur la boucle int?rieure, et apres avoir  
>> recherch? sur google et dans les manuels des diff?rents outils je  
>> n'ai trouv? nulle part une description exacte de ce que ces  
>> conditions signifient... Pouvez-vous m'aider l? aussi ?
>>
>> Je suis relativement nouveau dans le domaine des methodes  
>> formelles, et dans l'usage de l'outil, je ne sais donc pas bien  
>> s'il manque simplement une anotation quelquepart, ou s'il faut  
>> faire la preuve interactivement....
>>
>> Merci de votre aide,
>>
>> Romain Jobredeaux
>>
>>
>> _______________________________________________
>> Frama-c-discuss mailing list
>> Frama-c-discuss at lists.gforge.inria.fr
>> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss
>
>
> -- 
> Claude March?                          | tel: +33 1 72 92 59 69
> INRIA Saclay - ?le-de-France           | mobile: +33 6 33 14 57 93
> Parc Orsay Universit?                  | fax: +33 1 74 85 42 29
> 4, rue Jacques Monod - B?timent N      | http://www.lri.fr/~marche/
> F-91893 ORSAY Cedex                    |
>
>
>
>
>
>
>
>
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss
>

Frama-C-discuss mailing list archives

[Frama-c-discuss] boucles imbriquées