--- layout: fc_discuss_archives title: Message 47 from Frama-C-discuss on November 2011 ---
Hello, On 29/11/2011 19:39, Stephen Siegel wrote: > Below is an example that comes with the textbook Rigorous Software Development. > partition_swap_permut.c:32:[kernel] user error: invalid implicit conversion from 'int *' to 'int []' in annotation. > [kernel] user error: skipping file "partition_swap_permut.c" that has errors. > [kernel] Frama-C aborted because of invalid user input. > r > > I fixed this is a few other examples by just changing the parameter > type in the predicate to the pointer type. However, in this example, I'm > not sure if that fix will work. The problem is that in the definition of > Permut, there is a bound variable "a" of type "int[]" used in the > universal quantifier. I don't think I want to quantify over "int*". Any > suggestions? Having Permut and Swap act on pointers instead of arrays is indeed the correct way to do it. I can understand your concern about the universal quantification over pointers, that do not have a clean mathematical counterpart, but the definition will nevertheless be correct (in order to prove Permut{L1,L2}(a,l,h) for L1 != L2, you'll need to have access the elements *(a+(l..h)), on which you are able to say something non-trivial[1] only if \valid(a+(l..h)) holds) However, if it makes you feel more comfortable, you can explicit guards in your cases saying exactly that you consider only valid pointers: /*@ inductive Permut{L1,L2}(int a*, integer l, integer h) { case Permut_refl{L}: \forall int a*, integer l, h; \at(\valid(a+(l..h)),L) ==> Permut{L,L}(a, l, h) ; case Permut_sym{L1,L2}: \forall int a*, integer l, h; \at(\valid(a+(l..h)),L1) && \at(\valid(a+(l..h)),L2) ==> Permut{L1,L2}(a, l, h) ==> Permut{L2,L1}(a, l, h) ; case Permut_trans{L1,L2,L3}: \forall int a*, integer l, h; \at(\valid(a+(l..h)),L1) && \at(\valid(a+(l..h)),L2) && \at(\valid(a+(l..h)),L3) ==> Permut{L1,L2}(a, l, h)&& Permut{L2,L3}(a, l, h) ==> Permut{L1,L3}(a, l, h) ; case Permut_swap{L1,L2}: \forall int a*, integer l, h, i, j; \at(\valid(a+(l..h)),L1) && \at(\valid(a+(l..h)),L2) ==> l<= i<= h&& l<= j<= h&& Swap{L1,L2}(a, i, j) ==> Permut{L1,L2}(a, l, h) ; } @*/ Best regards, -- E tutto per oggi, a la prossima volta Virgile [1] other than e.g. *(a+i) == *(a+i) that holds whatever a and i are.