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

[Frama-c-discuss] Issue to express assigns on arrays



Hello,

I have following code:
------
#include <string.h>

#define MAX 12

int a[MAX];
char *c[MAX];

/*@ assigns a[..];
 */
void assign_int(void)
{
  int i;

  //@ loop invariant 0 <= i && i <= MAX;
  for (i = 0; i < MAX; i++) {
    a[i] = 0x45;
  }
}

/*@ assigns c[..];
 */
void assign_char(void)
{
  int i;

  //@ loop invariant 0 <= i && i <= MAX;
  for (i = 0; i < MAX; i++) {
    c[i] = strndup("something", MAX);
  }
}

/*@ assigns a[..];
    assigns c[..];
 */
void main(void)
{
  assign_int();
  assign_char();
}
------

On this code, I cannot prove properties "assigns a[..];" for
assign_int() and "assigns c[..];" for assign_char(). However the
assignation seems obvious to me.

I have tried "assigns a[0..11];" without success.

Could somebody explain to me what I have overlooked?

Yours,
david