--- layout: fc_discuss_archives title: Message 29 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, 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]$



-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20140929/7c38c729/attachment.html>