--- layout: fc_discuss_archives title: Message 21 from Frama-C-discuss on January 2009 ---
Hallo Christoph, Le jeu 08 jan 2009 13:03:47 CET, "Christoph Weber" <Christoph.Weber at first.fraunhofer.de> a ?crit : > /*@ axiomatic Predicate_remove_copy { > > logic integer predicate_remove_copy{La,Lb}(int* a, int* b, integer i_a, integer i_b, int value); > } > */ > int remove_copy_array (int* a, int length, int* dest, int value ) > { > int i_a = 0; > int i_dest = 0; > > > /*@ > loop invariant i_dest == predicate_remove_copy{Pre,Here}(a, dest, i_a-1, i_dest-1, value); > */ > for ( ; i_a != length; ++i_a) > if (a[i_a] != value) > { > dest[i_dest] = a[i_a]; > ++i_dest; > } I guess that your issue stems from the fact that your axioms defining predicate_remove_copy (by the way it is rather a function than a predicate) always compare the value of predicate_remove_copy on the same two states La and Lb. I'd say that you need at least one axiom saying that if the values contained in b in states Lb1 and Lb2 are the same, then predicate_remove_copy returns the same result, i.e. axiom predicate_remove_copy_label{La,Lb1,Lb2}: \forall int* a, int* b, value, integer i_a, i_b; (\forall integer i; 0<= i <= i_b ==> \at(b[i],Lb1) == \at(b[i],Lb2)) ==> predicate_remove_copy{La,Lb1}(a,b,i_a,i_b,value) == predicate_remove_copy{La,Lb2}(a,b,i_a,i_b,value); In addition, adding an assertion in the loop after the update of dest[i_dest] seems to help the provers figuring out which instances of predicate_remove_copy need to be considered: /*@assert i_dest+1==predicate_remove_copy{Pre,Here}(a,dest,i_a,i_dest,value); */ With these two additions, all goals are proved by alt-ergo and Z3 (but Simplify fails to prove the assertion) -- E tutto per oggi, a la prossima volta. Virgile