--- layout: fc_discuss_archives title: Message 33 from Frama-C-discuss on September 2014 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] [kernel] user error: skipping file "selection.c" that has errors.



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
>