frama-c [ядро] ошибка пользователя: пропуск файла selection.c, в котором есть ошибки

Я новый пользователь Frama-c. Я только что установил Neon-20140301 и почему 2.34 в моей системе Fedora 14 с компилятором Ocaml 4.01.0.

В режиме без графического интерфейса установка прошла успешно.

Однако, когда я попытался запустить некоторые примеры из Why2.34, я получил несколько ошибок, подобных следующим: Кажется, проблема с совместимостью.

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

frama-c
person luke    schedule 29.09.2014    source источник

Ответы (1)


arrow_upward
0
arrow_downward

Вопрос был задан в двух экземплярах в списке рассылки и ответил Клод Марше:

Примеры в каталоге examples-c/, почему это старые примеры, использующие синтаксис Caduceus, своего рода предшественник Frama-C.

Актуальные примеры можно найти в каталогеtests/c/, а также в нескольких других местах, например. «ACSL на примерах» и др.

person Pascal Cuoq    schedule 08.10.2014