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

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