--- layout: fc_discuss_archives title: Message 59 from Frama-C-discuss on September 2010 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] frama-c outputs errors in jessie tutorial



Hello,

I am trying frama-c using tutorials provided on the web site frama-c.com, 
especially the jessie tutorial: http://frama-c.com/jessie_tutorial_index.html 
and I have a problem with the section 3.2  ?Advanced Algebraic Modeling?

frama-c outputs errors when it analyses ACSL specifications, here is the 
output:

prompt> frama-c -jessie sorting.c
[kernel] preprocessing with "gcc -C -E -I.  -dD sorting.c"
sorting.c:7:[kernel] user error: Error during annotations analysis: invalid 
implicit conversion from int * to int []
[kernel] user error: skipping file "sorting.c" that has errors.
[kernel] Frama-C aborted because of an invalid user input.

The line 7 is ? @ ensures Swap{Old,Here}(t,i,j);  ?, but the type ?int *? is 
never used in this program. So I do not now what is the problem and how to 
correct it.

Anyone has an idea ?

I'm using the version Boron-20100401

Thank you 

I copy the tutotrial example below (to avoid you to go to see the tutorial: 
http://frama-c.com/jessie_tutorial_index.html#htoc13):

--- sorting.h --------------------
/*@ 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) ; 
  @ } 
  @*/ 
 
/*@ predicate Sorted{L}(int a[], integer l, integer h) = 
  @   \forall integer i; l <= i < h ==> a[i] <= a[i+1] ; 
  @*/ 
-- end sorting.h ---------------


--- sorting.c --------------------
#pragma JessieIntegerModel(math) 
 
#include "sorting.h" 
 
/*@ requires \valid(t+i) && \valid(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; 
} 
     
/*@ requires \valid_range(t,0,n?1); 
  @ behavior sorted: 
  @   ensures Sorted(t,0,n?1); 
  @ behavior permutation: 
  @   ensures Permut{Old,Here}(t,0,n?1); 
  @*/ 
void min_sort(int t[], int n) { 
  int i,j; 
  int mi,mv; 
  if (n <= 0) return; 
  /*@ loop invariant 0 <= i < n; 
    @ for sorted:  
    @  loop invariant  
    @   Sorted(t,0,i) &&  
    @   (\forall integer k1, k2 ;  
    @      0 <= k1 < i <= k2 < n ==> t[k1] <= t[k2]) ; 
    @ for permutation: 
    @  loop invariant Permut{Pre,Here}(t,0,n?1); 
    @ loop variant n?i; 
    @*/ 
  for (i=0; i<n-1; i++) { 
    // look for minimum value among t[i..n?1] 
    mv = t[i]; mi = i; 
    /*@ loop invariant i < j && i <= mi < n; 
      @ for sorted:  
      @  loop invariant 
      @    mv == t[mi] && 
      @    (\forall integer k; i <= k < j ==> t[k] >= mv); 
      @ for permutation: 
      @  loop invariant 
      @   Permut{Pre,Here}(t,0,n?1); 
      @ loop variant n?j; 
      @*/ 
    for (j=i+1; j < n; j++) { 
      if (t[j] < mv) {  
        mi = j ; mv = t[j];  
      } 
    } 
    swap(t,i,mi); 
  } 
} 
-- end sorting.c ---------------