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

[Frama-c-discuss] Array elements passed as reference



Hello,

Consider the code below (example code from bug http://bts.frama-c.com/view.php?id=38). Copy is called with array elements passed as reference.

In the absence of a modifies-clause, which of the following assumptions does Jessie make in this situation?
  1) Copy may modify arbitrary elements in a[]
  2) Copy may modify at most a[0] and a[i]

Regards,
Boris

-------------------------------

void Copy(int *p, int *q)
{
  *q = *p;
}


int foo(int a[]) {
  int i=1;

  Copy(&a[0], &a[i]);
  return i;
}