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

  • Subject: [Frama-c-discuss] Unability to verify an arithmetic assertion disapears in a reduced but similar test case
  • From: dmentre at linux-france.org (David MENTRE)
  • Date: Wed, 18 Mar 2009 16:31:52 +0100
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.