--- layout: fc_discuss_archives title: Message 61 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



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


-- 
Claude March?                          | tel: +33 1 72 92 59 69
INRIA Saclay - ?le-de-France           | mobile: +33 6 33 14 57 93
Parc Orsay Universit?                  | fax: +33 1 74 85 42 29
4, rue Jacques Monod - B?timent N      | http://www.lri.fr/~marche/
F-91893 ORSAY Cedex                    |