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