Frama-C-discuss mailing list archives

kydeza at gmail.com (kydeza) · Thu, 30 Sep 2010 15:25:19 +0200

Thank you,

I have replaced ?int a[]? by ?int *a? everywhere in sorting.h and it is ok 
now.

Thank you

En r?ponse au message de Claude Marche <Claude.Marche at inria.fr>
envoy? jeudi 30 septembre 2010 ? 15:10
?: ? : "Frama-C public discussion" <frama-c-discuss at lists.gforge.inria.fr>
Sujet: Re: [Frama-c-discuss] frama-c outputs errors in jessie tutorial
> On 09/30/2010 02:38 PM, kydeza wrote:
> > 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 ?
> 
> It is a mistake in the doc, sorry.
> 
> Please replace int a[] by int *a in the parameters of Swap, Permut,
> Sorted declarations
> 
> Since ACSL-Boron, there is a difference between int[] and int* in the
> logic annotations.
> 
> - Claude
> 
> > 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 ---------------
> > 
> > _______________________________________________
> > 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