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

[Frama-c-discuss] [Jessie] pset_disjoint



Hello,

I'm unable to verify the code below. It seems that Jessie requires that p and q are pointers to distinct memory locations. However, this is not required by Copy.
Is this a bug?

Regards,
Boris


/*@ requires \valid(p) && \valid(q);
*/
void Copy(int *p, int *q)
{
  *q = *p;
}

void foo() {
  int a[] = {1,2,3};

  Copy(&a[1], &a[1]);
}