--- layout: fc_discuss_archives title: Message 30 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.



Hello,

Le 29/09/2014 05:35, luoq at ustc.edu.cn a ?crit :
> It seems that there is a compatibility problem.

No, there is a syntax issue in your example.


> [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 ''

As Frama-C says, you have a syntax error at line 4...

> [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

...indeed, you forgot the semicolon (";") at the end of the line.

For further references, look at Figure 2.14, p. 49 of ACSL reference 
manual. You can also look at examples in the same and previous pages.

It would help to learn to read error messages.

Best regards,
david