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] Unability to verify an arithmetic assertion disapears in a reduced but similar test case

Le mer 18 mar 2009 16:31:52 CET,
David MENTRE <dmentre at linux-france.org> a ?crit :

> Hello,
> 
> I have following test case :
> ===
> #define MAX 1000
> #define N 4
> 
> int counters[N];
> 
> /*@ requires \forall int i; 0 <= i < N ==> counters[i] >= 0 &&
> counters[i] < MAX;
>     requires 0 <= n && n <= N;
>     assigns \nothing;
>  */
> int f(int n)
> {
>   int total = 0;
>   int total_min_0;
>   int i;
> 
>   /*@ loop invariant total >= 0;
>       loop invariant 0 <= i && i <= n;
>       loop invariant total <= i * MAX;
>    */
>   for (i = 0; i < n; i++) {
>     total += counters[i];
>   }
> 
>   /* assert total >= counters[0];
>    */
>   total_min_0 = total - counters[0];
> 
>   return total_min_0;
> }
> 
> void main(void)
> {
>   counters[0] = 1;
>   counters[1] = 0;
>   counters[2] = 3;
>   counters[3] = 4;
>   f(N);
>   return;
> }

> For me the code is exactly the same as in the reduced test case
> (except that "num_candidates" is a global variable instead of a
> function parameter). However, on this code, I am unable to prove the
> assertion "assert total >= counters[0];", while exactly the same
> assertion is proven in the reduced test case without any issue. That's
> puzzling me!

if the code of the reduced example is exactly like above, the assertion
is not proved, since the lack of '@' means that it is not seen as an
ACSL annotation. If you put back the '@', there is another issue: the
assertion is false. Namely, if you call f with n == 0, the loop is not
entered, and total is still 0 at this point.

Now the larger example has a stronger pre-condition (0<
num_candidates). So why does alt-ergo still fail on the assertion? 
Well, remember that the only thing that jessie 'knows' after a loop is
its invariant, and here the loop invariant is too weak: it gives an
upper bound for total, but no lower bound. A possibility (short of the
ACSL construction \sum which is currently unsupported by jessie) would
be to add the following invariant:

loop invariant \forall integer j; 0<=j<i ==> total >= counters[j];

Best regards,
-- 
E tutto per oggi, a la prossima volta.
Virgile