--- layout: fc_discuss_archives title: Message 14 from Frama-C-discuss on January 2009 ---
Hello and a happy new year, today I am trying to modify an implementation and still concur with the function contract. Therefore following code first: /*@ requires 0 <= length; requires \valid_range (a, 0, length-1); requires \valid_range (b, 0, length-1); assigns \nothing; behavior equal: ensures \result == 1 <==> (\forall integer i; 0 <= i < length ==> a[i] == b[i]); behavior not_equal: ensures \result == 0 <==> (\exists integer i; 0 <= i < length && a[i] != b[i]); */ int equal_array (int* a, int length, int* b ) { int index_a = 0; int index_b = 0; /*@ loop invariant 0 <= index_a <= length; loop invariant 0 <= index_b <= length; loop invariant index_a == index_b; loop invariant \forall integer k; 0 <= k < index_a ==> a[k] == b[k]; */ while ( index_a != length ) { if (a[index_a] != b[index_b]) return 0; ++index_a; ++index_b; } return 1; } Since I am using "assigns \nothing;" I expect the term \old() in comparison to be obsolete. But as I recall, assigns \nothing allows temorary modification, as long as the content of the elements mentioned in the parameter list of the function is restored before termination. So I modified the algorithm, to alter the memory and restore it, allowing the algorithm to return allways "true": /*@ requires 0 <= length; requires \valid_range (a, 0, length-1); requires \valid_range (b, 0, length-1); assigns \nothing; behavior equal: ensures \result == 1 <==> (\forall integer i; 0 <= i < length ==> a[i] == b[i]); behavior not_equal: ensures \result == 0 <==> (\exists integer i; 0 <= i < length && a[i] != b[i]); */ int equal_array (int* a, int length, int* b ) { int save_array_a[length]; int save_array_b[length]; /*@ loop invariant 0 <= i <= length; loop invariant \forall integer k; 0 <= k < i ==> a[k] == b[k] == 0; loop invariant \forall integer k; 0 <= k < i ==> a[k] == save_array_a[k]; loop invariant \forall integer k; 0 <= k < i ==> b[k] == save_array_b[k]; */ for(int i = 0; i < length; i++) { save_array_a[i] = a[i]; save_array_b[i] = b[i]; a[i] = 0; b[i] = 0; } int index_a = 0; int index_b = 0; /*@ loop invariant 0 <= index_a <= length; loop invariant 0 <= index_b <= length; loop invariant index_a == index_b; loop invariant \forall integer k; 0 <= k < index_a ==> a[k] == b[k]; */ while ( index_a != length ) { if (a[index_a] != b[index_b]) return 0; ++index_a; ++index_b; } /*@ loop invariant 0 <= i <= length; loop invariant \forall integer k; 0 <= k < i ==> a[k] == save_array_a[k]; loop invariant \forall integer k; 0 <= k < i ==> b[k] == save_array_b[k]; */ for(int i = 0; i < length; i++) { a[i] = save_array_a[i]; b[i] = save_array_b[i]; } return 1; } My problem: I cannot invoke the Jessie gui, it stops with the message: equal_array.c:6: Warning: Variable-sized local variable save_array_a equal_array.c:7: Warning: Variable-sized local variable save_array_b Cleaning unused parts Symbolic link Starting semantical analysis Starting Jessie translation No code for function __builtin_alloca, default assigns generated Producing Jessie files in subdir equal_array.jessie File equal_array.jessie/equal_array.jc written. File equal_array.jessie/equal_array.cloc written. Calling Jessie tool in subdir equal_array.jessie Generating Why function equal_array File "jc/jc_interp.ml", line 861, characters 11-11: Uncaught exception: File "jc/jc_interp.ml", line 861, characters 11-17: Assertion failed Jessie subprocess failed: jessie -why-opt -split-user-conj -v -locs e qual_array.cloc equal_array.jc My question: Is this indended, signaling me to stop fooling around or am I missing something to invoke the gui properly. Cheers Christoph -------------- next part -------------- An HTML attachment was scrubbed... URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20090107/234b610c/attachment.htm