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

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; 
}