Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[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