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



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;
}
===

All invariant and properties are proven without any issue using
alt-ergo, especially the assertion "assert total >= counters[0];".

Now my real program is like this (I have deleted uneeded lines) :

===
#define MAX_CANDIDATES 20
#define MAX_VOTES_PER_CANDIDATE 100000

int num_candidates;
int counters[MAX_CANDIDATES] = { 0, };

[...]

/*@ requires 0 < num_candidates && num_candidates < MAX_CANDIDATES;
    requires \forall int i; 0 <= i < MAX_CANDIDATES ==> counters[i] <
MAX_VOTES_PER_CANDIDATE && counters[i] >= 0;
    assigns \nothing;
 */
void compute_results(void)
{
  int total = 0;
  int i, winner, valid_total;

  /*@ loop invariant 0 <= i && i <= num_candidates;
      loop invariant 0 <= counters[i] < MAX_VOTES_PER_CANDIDATE;
      loop invariant total >= 0;
      loop invariant total <= i * MAX_VOTES_PER_CANDIDATE;
  */
  for (i = 0; i < num_candidates; i++) {
    total += counters[i];
  }
  //@ assert total < MAX_CANDIDATES * MAX_VOTES_PER_CANDIDATE;
  //@ assert total >= counters[0];
  //@ assert counters[0] >= 0;
  valid_total = total - counters[0];
}
===

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!

What I am missing? Is there something I haven't seen?

Many thanks in advance for any light,
Sincerely yours,
david

PS: I can provide the full code on request, I just don't want to make it public.