# 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.

# [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,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,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

```