--- layout: fc_discuss_archives title: Message 32 from Frama-C-discuss on January 2012 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Jessie plug-in - Pointer arithmetic



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>