--- layout: fc_discuss_archives title: Message 18 from Frama-C-discuss on January 2009 ---
Hello, now I have a rather complex example, which I need some advice with before posting it on the BTS The function reverse uses a swap function to reverse the elements of an array: #include "swap.h" /*@ requires 0 <= length; requires \valid_range (a, 0, length-1); ensures \forall integer k; 0 <= k < length ==> \old(a[k]) == a[length-1-k] && a[k] == \old(a[length-1-k]); */ void reverse_array (int* a, int length) { int index_a = 0; int index_backwards = length; /*@ loop invariant 0 <= index_a <= length; loop invariant 0 <= index_backwards <= length; loop invariant index_a == length - index_backwards; loop invariant \forall integer k; 0 <= k < index_a ==> \at(a[k],Pre) == a[length-1-k] && a[k] == \at(a[length-1-k],Pre); */ while ((index_a != index_backwards) && (index_a != --index_backwards)) swap_user (&a[index_a++], &a[index_backwards]); } File "swap.h" ======== /*@ requires \valid(a); requires \valid(b); ensures *a == \old(*b); ensures *b == \old(*a); */ void swap_user (int* a, int* b ); File "swap.c" ======== #include "swap.h" void swap_user (int* a, int* b ) { int c = *a; *a = *b; *b = c; } When invoking the Gui for reverse_array() I get the error: Cleaning unused parts Symbolic link Starting semantical analysis Starting Jessie translation No code for function swap_user, default assigns generated Producing Jessie files in subdir reverse_array.jessie File reverse_array.jessie/reverse_array.jc written. File reverse_array.jessie/reverse_array.cloc written. Calling Jessie tool in subdir reverse_array.jessie Generating Why function reverse_array Calling VCs generator. make[1]: Entering directory `/cygdrive/d/Eigene Dateien/StudienUnterlagen/Praxis semester/SVN/trunk/Framac/own-examples/ProvableSTL/reverse/reverse_array.jessie' gwhy-bin [...] why/reverse_array.why Computation of VCs... File "why/reverse_array.why", line 1158, characters 101-117: Application to int_P_int_M_a_22 creates an alias make[1]: *** [reverse_array.stat] Error 1 make[1]: Leaving directory `/cygdrive/d/Eigene Dateien/StudienUnterlagen/Praxiss emester/SVN/trunk/Framac/own-examples/ProvableSTL/reverse/reverse_array.jessie' Jessie subprocess failed: make -f reverse_array.makefile gui I would like to know whether the mistake is mine or if I have to post on the BTS Cheers Christoph -------------- next part -------------- An HTML attachment was scrubbed... URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20090107/ae67bb9b/attachment.htm