Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[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.