--- layout: fc_discuss_archives title: Message 34 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



Hello B?rbara,

On 19/01/2012 12:33, B?rbara Vieira wrote:
> @ 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);

Jessie is right: your loop invariant is not correct. Namely, in your 
formula, array is a logical variable. Hence, its value does not depend 
on a given C memory state, and you have \at(array,L3) == \at(array,L2), 
for any L2,L3 (thus \at(array,L3) != \at(array,L2)+1). If you want to 
use this inductive to write your invariant, you have to use two distinct 
logical variables array1 and array2 in your inductive case:
  \forall unsigned int len1,len2,len3;
      \forall unsigned int* result;
      \forall unsigned int* array1,*array2;
      loop1{L1,L2}(len1,len2,result,array1) ==>
       len3 == len2 -1 ==>
       \at(*result,L3) == (\at(*result,L2) & \at(array1[0],L2)) ==>
       array2 == array1 + 1 ==>     //Line that corresponds to array++
       loop1{L1,L3}(len1,len3,result,array2);

(BTW, I'm not sure you need two distincts len arguments in loop1, this 
could be handled similarly).

-- 
E tutto per oggi, a la prossima volta
Virgile