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