--- layout: fc_discuss_archives title: Message 64 from Frama-C-discuss on March 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Global initialization of variables not taken into account?



Hello,

Suppose I have following code:
===
#define MAX 5
int c[5] = {0, };
int global = 0;

void main(void)
{
  //@ assert global == 0;
  //@ assert \forall integer i; 0 <= i < MAX ==> c[i] == 0;

  return;
}
===

The two assertions are not proven by Alt-Ergo (\?/ state[1]).

However, if I write the code like this:
===
#define MAX 5
int c[5];
int global;

void main(void)
{
  int i;

  /*@ loop invariant \forall integer j; 0 <= j < i ==> c[j] == 0;
      loop invariant 0 <= i && i <= MAX;
   */
  for (i = 0; i < MAX; i++)
    c[i] = 0;
  global = 0;

  //@ assert global == 0;
  //@ assert \forall integer i; 0 <= i < MAX ==> c[i] == 0;

  return;
}
===

My assertions are correctly proven. Am I forced to do all global
initializations manually or I have missed something? This is not a big
issue but is a bit cumbersome.

I'm calling Jessie like this:
  frama-c -jessie-analysis -jessie-atp alt-ergo -jessie-cpu-limit 2
-jessie-gui init-issue.c

Sincerely yours,
david

[1] What does that exactly mean? (cf.
http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2009-March/000425.html)