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] frama-c outputs errors in jessie tutorial

  • Subject: [Frama-c-discuss] frama-c outputs errors in jessie tutorial
  • From: kydeza at gmail.com (kydeza)
  • Date: Thu, 30 Sep 2010 14:38:02 +0200
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 ---------------