--- layout: fc_discuss_archives title: Message 44 from Frama-C-discuss on October 2008 ---
Christoph Weber wrote: > Hi and a thank you for the help, > > but I like to continue questioning where I stopped. > > You remember the array_cpy: > /*@ > requires 0 < n; > requires \valid_range(a, 0, n-1) && \valid_range(b, 0, n-1)&& disjoint_arrays(a, b, n); > ensures \forall int k; 0 <= k < n ==> a[k] == b[k]; > */ > void array_cpy(int* a, int n, int* b) > { > /*@ > loop invariant 0 <= i <= n && \forall int m; 0 <= m < i ==> a[m] == b[m]; > */ > for (int i = 0;i < n;i++) > { > a[i] = b[i]; > } > } > > This works fine with the Hydrogen-version on Win 32 and the Z3 prover. On the Helium edition on OSX it terminates successfully with CVC3 (Z3 not aviable). Now I'd like to know: > - what has to be done or added to let ergo v0.8 or simplify verify it as well. You have to improve ergo and simplify :-) One advice is to use "integer" instead of ints in your annotations: ensures \forall integer k; 0 <= k < n ==> a[k] == b[k]; and so on. > - array_cpy is only partial specified on my opinion the ensures clause has to be altered to > ensures \forall int k; 0 <= k < n ==> a[k] == \old(b[k]); > using this I receive an error due to preservation of loop invariant. I think the comparison in the loop invariant has to be altered to > a[m] == \at(b[m],Old); > but FramaC will return > File array_test.c, line 28, characters 80-93: > Error during analysis of annotation: logic label `Old' not found > array_test.c:29: Warning: ignoring logic loop annotation > I tried a bit but I where unable to cheat my way around. Old does not mean anything in loop invariants. You have to use Pre: a[m] == \at(b[m],Pre)