--- layout: fc_discuss_archives title: Message 63 from Frama-C-discuss on September 2010 ---
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