--- layout: fc_discuss_archives title: Message 29 from Frama-C-discuss on October 2008 ---
Hello, I'm exercising with the jessie-tool learn the usage of the ACSL-Language. I have two examples. My Problem is with the second one. #1: works fine, i get green bullets /*@ requires 0 < n; requires \valid_range(a, 0, n-1); ensures \forall int i; 0 <= i < n ==> a[i] == 0; */ void array_zero(int* a, int n){ /*@ loop invariant 0 <= i <= n && \forall int k; 0 <= k < i ==> a[k] == 0; */ for(int i = 0;i< n;i++){ a[i]=0; } } #2: in the second example the preservation of the loop invariant wont work /*@ requires 0 < n; requires \valid_range(a, 0, n-1) && \valid_range(b, 0, n-1); 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]; } } What am I missing, to get the examples running? Christoph -------------- next part -------------- An HTML attachment was scrubbed... URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20081009/7620ab3b/attachment.htm