--- layout: fc_discuss_archives title: Message 47 from Frama-C-discuss on November 2011 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] pointer/array issue



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.