--- layout: fc_discuss_archives title: Message 45 from Frama-C-discuss on March 2009 ---
[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