--- layout: fc_discuss_archives title: Message 30 from Frama-C-discuss on September 2014 ---
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