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

  • Subject: [Frama-c-discuss] pointer/array issue
  • From: sylvain.nahas at googlemail.com (sylvain nahas)
  • Date: Wed, 14 Dec 2011 12:01:30 +0100
  • In-reply-to: <31902097-FACD-4679-9C62-73267E2D8591@udel.edu>
  • References: <7BAFF59B-AA79-4F29-83A8-044C1466E82C@UDel.Edu> <CAOH62JiDQTes35ueRGd2M60GnxE9GKv-Kz1psANTo5auVdwtBg@mail.gmail.com> <CAM6WbQfg_GqA+VsQVvxywJw6RY_0aYYX91XtUx0urahjwETJGA@mail.gmail.com> <392D90D4-56AD-4A21-9865-BEBE5D04546A@udel.edu> <CAM6WbQcs6k++LgnEhAaknFmc9fBPEfcyx=E_z7B4i_YR9U=Q3A@mail.gmail.com> <F0793D8F-8337-4DD4-A379-E816EA5991F4@udel.edu> <CAM6WbQc89+2xrYgEfDkFcUVi7gAT_qCqyC+PrK_HojH97mC=ow@mail.gmail.com> <1447A980-94B1-4EA1-B7B3-9A9B55F2C056@udel.edu> <5E3974C2-BABB-4BBD-AC11-0AD7D4193E40@first.fraunhofer.de> <31902097-FACD-4679-9C62-73267E2D8591@udel.edu>
Hi Stephen,

if you adapt the examples of the book to newer versions of Frama-C,
would that be possible that you make the result public?
I for one would be very happy if you could you do that.

This book seems to be one of the very few tutorial resources available
for Frama-C, and the most adapted for self-study for programmers to
whom formal methods are new. That would be very sad indeed that
compatibility breaks render it unusable, especially since it has been
published only very recently!

thanks,
Sylvain



On Tue, Nov 29, 2011 at 7:39 PM, Stephen Siegel <siegel at udel.edu> wrote:
> Below is an example that comes with the textbook Rigorous Software Development.
> It was used with an earlier version of Frama-C.
> In the Carbon version, there is an error:
>
> rsd$ frama-c -jessie partition_swap_permut.c
> [kernel] preprocessing with "gcc -C -E -I. ?-dD partition_swap_permut.c"
> 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?
>
> Thx,
> Steve
>
>
>
>
> /*@ predicate Swap{L1,L2}(int a[], integer i, integer j) =
> ?@ ? \at(a[i],L1) == \at(a[j],L2) &&
> ?@ ? \at(a[j],L1) == \at(a[i],L2) &&
> ?@ ? \forall integer k; k != i && k != j
> ?@ ? ? ? ==> \at(a[k],L1) == \at(a[k],L2);
> ?@*/
>
> /*@ inductive Permut{L1,L2}(int a[], integer l, integer h) {
> ?@ ?case Permut_refl{L}:
> ?@ ? \forall int a[], integer l, h; Permut{L,L}(a, l, h) ;
> ?@ ?case Permut_sym{L1,L2}:
> ?@ ? ?\forall int a[], integer l, h;
> ?@ ? ? ?Permut{L1,L2}(a, l, h) ==> Permut{L2,L1}(a, l, h) ;
> ?@ ?case Permut_trans{L1,L2,L3}:
> ?@ ? ?\forall int a[], integer l, h;
> ?@ ? ? ?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;
> ?@ ? ? ? l <= i <= h && l <= j <= h && Swap{L1,L2}(a, i, j) ==>
> ?@ ? ? Permut{L1,L2}(a, l, h) ;
> ?@ }
> ?@*/
>
>
>
>
> /*@ requires \valid_index(t,i) && \valid_index(t,j);
> ?@ assigns t[i],t[j];
> ?@ ensures Swap{Old,Here}(t,i,j);
> ?@*/
> void swap(int t[],int i,int j) {
> ?int tmp = t[i];
> ?t[i] = t[j];
> ?t[j] = tmp;
> }
>
>
> /* Quicksort Partition Function */
>
> /*@ requires 0 <= p <= r && \valid_range(A,p,r);
> ?@ ensures
> ?@ ? ? Permut{Old,Here}(A,p,r);
> ?@*/
> int partition (int A[], int p,int r)
> {
> ?int x = A[r];
> ?int tmp, j, i = p-1;
>
> ?/*@ loop invariant
> ? ?@ ? ?p <= j <= r && p-1 <= i < j &&
> ? ?@ ? ?Permut{Pre,Here}(A,p,r);
> ? ?@ loop variant (r-j);
> ? ?@*/
> ?for(j=p; j<r; j++)
> ? ?if (A[j] <= x) {
> ? ? ?i++;
> ? ? ?swap(A,i,j);
> ? ?}
> ?swap(A,i+1,r);
> ?return i+1;
> }
>
>
>
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss