--- layout: fc_discuss_archives title: Message 33 from Frama-C-discuss on September 2014 ---
Hi, The examples in directory examples-c/ of why are old examples using Caduceus syntax, a kind of predecessor of Frama-C. Up-to-date examples can be found in directory tests/c/ instead, and also in several other places, e.g. "ACSL by examples", etc. Sorry for the inconvenience. - Claude On 09/29/2014 05:35 AM, luoq at ustc.edu.cn wrote: > Hi, everyone, > > I am a new user of Frama-c. I just installed Neon-20140301 and why 2.34 > on my Fedora 14 system with Ocaml compiler 4.01.0. > > Under no-GUI mode, install was successful. > > However, when I tried to run some examples from why2.34, I got several > errors like the following: > It seems that there is a compatibility problem. > > Is there any way to solve this? > > > Thanks in advance! > > > -------------------------------------------------------------------------------- > > [user /data/Down/why-2.34/examples-c/sorting]$ frama-c -jessie selection.c > [kernel] preprocessing with "gcc -C -E -I. -dD selection.c" > selection.c:4:[kernel] user error: unexpected token '' > [kernel] user error: skipping file "selection.c" that has errors. > [kernel] Frama-C aborted: invalid user input. > [user /data/Down/why-2.34/examples-c/sorting]$ cat selection.c > > /* Selection sort */ > > //@ type intmset > > //@ logic intmset mset(int t[],int i,int j) reads t[..] > > /*@ requires \valid_index(t,i) && \valid_index(t,j) > @ assigns t[i],t[j] > @ ensures t[i] == \old(t[j]) && t[j] == \old(t[i]) > @*/ > void swap(int t[],int i,int j) { > int tmp = t[i]; > t[i] = t[j]; > t[j] = tmp; > } > > /*@ predicate sorted(int t[],int i,int j) { > @ \forall int k; i <= k < j => t[k] <= t[k+1] > @ } > @*/ > > /*@ requires n >= 1 && \valid_range(t,0,n-1) > @ assigns t[0..n-1] > @ ensures sorted(t,0,n-1) && mset(t,0,n-1) == \old(mset(t,0,n-1)) > @*/ > void selection(int t[], int n) { > int i,j,min; > init: > /*@ // t[0..i-1] is already sorted > @ invariant > @ 0 <= i <= n-1 && > @ sorted(t, 0, i-1) && > @ mset(t,0,n-1) == \at(mset(t,0,n-1),init) && > @ \forall int k; \forall int l; 0 <= k < i => > @ i <= l < n => t[k] <= t[l] > @ loop_assigns > @ t[0..n-1] > @ variant > @ n - i > @*/ > for (i=0; i < n-1; i++) { > /* we look for the minimum of t[i..n-1] */ > min = i; > /*@ invariant > @ i+1 <= j <= n && > @ i <= min < n && > @ \forall int k; i <= k < j => t[min] <= t[k] > @ variant > @ n - j > @*/ > for (j = i + 1; j < n; j++) { > if (t[j] < t[min]) min = j; > } > /* we swap t[i] and t[min] */ > swap(t,min,i); > } > } > > [user /data/Down/why-2.34/examples-c/sorting]$ > > > > > > _______________________________________________ > 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 >