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