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] Jessie plug-in - Pointer arithmetic

  • Subject: [Frama-c-discuss] Jessie plug-in - Pointer arithmetic
  • From: barbaraisabelvieira at gmail.com (Bárbara Vieira)
  • Date: Thu, 19 Jan 2012 11:33:15 +0000
Hi everyone,

I'm trying to verify the following code:

void increment_ptr(unsigned int* array, unsigned int len, unsigned int* result)
{
	*result = 0xffaabbcc;
	while(len > 0) { *result &= array[0];  array++;  len--; }
}

using the Jessie plug-in/Frama-C Nitrogen.

In order to get a proper loop invariant I decided to write it as an inductive predicate (as I always do).
However, something that I really don't understand happens:
	- If I comment the line referent to array variable increment, the preservation of the loop invariant is (automatically) proved;
	- If I do not comment this line, I cannot prove the proof obligation related with the loop invariant preservation.
For both cases, the corresponding line of the inductive predicate is commented. 
Please check the annotated code below.

I was wondering if the problem is that Jessie does not support pointer arithmetic, however I found the following post 
http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2008-July/000581.html
in the Frama-C mailing list.

I tried to find something related to this in the mailing list, but I didn't succeed.
Does anybody can help me?!


Best regards,
B?rbara


---
B?rbara Vieira 
HasLab / INESC TEC
Dep. Inform?tica - Universidade do Minho

-----------------------------------------------------------------------------------------------------------------------------------------------------------

/*@ inductive loop1{L1,L2}( unsigned int len1, unsigned int len2, unsigned int* result, unsigned int* array){
 @   case base_case{L}:
 @     \forall unsigned int len;
 @     \forall unsigned int* result;
 @     \forall unsigned int* array; 
 @     loop1{L,L}(len,len,result,array);
 @   case ind_case{L1,L2,L3}:
 @     \forall unsigned int len1,len2,len3;
 @     \forall unsigned int* result; 
 @     \forall unsigned int* array; 
 @     loop1{L1,L2}(len1,len2,result,array) ==>
 @     len3 == len2 -1 ==> 
 @     \at(*result,L3) == (\at(*result,L2) & \at(array[0],L2)) ==>
 @     //\at(array,L3) == \at(array,L2) + 1 ==>	    					//Line that corresponds to array++
 @     loop1{L1,L3}(len1,len3,result,array);
 @ }
 @*/


/*@ requires len > 1 && \valid(array + (0..(len-1))) && \valid(result);
  @*/
void increment_ptr(unsigned int* array, unsigned int len, unsigned int* result)
{
	*result = 0xffaabbcc;

	//@ assert \valid(array+0);

	//@ ghost unsigned int old_len = len;

	//@ ghost goto L1;
	//@ ghost L1:

	
	/*@ loop invariant 0<=len<=old_len;
	  @ loop invariant loop1{L1,Here}(old_len,len,result,array);           
	  @ loop variant len;
	  @*/
	while(len > 0)
	{
		*result &= array[0];
		//array++;
		len--;
	}

}


-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20120119/3fdbfae7/attachment.htm>