--- layout: fc_discuss_archives title: Message 32 from Frama-C-discuss on June 2009 ---
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]); }