--- layout: fc_discuss_archives title: Message 45 from Frama-C-discuss on October 2008 ---
Thanks for the advice with the integer. But if I am using the Pre Label I don't meet the ensures requirements, or at least I don't get a green bullet. Currently I'm stuck with an other Problem. Within some annotated string.h examples I found a dereferenced \result. /*@ requires last > first; requires \valid_range(first, 0, last-first-1); ensures *\result == value; */ int* find_int_array (int* first, int* last, int value ); Attempts to apply it to my example will result in the following error. Fatal error: exception Assert_failure("src/jessie/interp.ml", 336, 14) do I get it due to my Hydrogen version ? Christoph ----- Original Message ----- From: "Claude March?" <Claude.Marche@inria.fr> To: "Christoph Weber" <Christoph.Weber@first.fraunhofer.de> Cc: <frama-c-discuss@lists.gforge.inria.fr> Sent: Monday, October 13, 2008 1:51 PM Subject: Re: [Frama-c-discuss] Specification Examples > > > 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) > > > > > > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss@lists.gforge.inria.fr > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss >