1

我是 Frama-c 的新用户。我刚刚使用 Ocaml 编译器 4.01.0 在我的 Fedora 14 系统上安装了 Neon-20140301 以及为什么要安装 2.34。

在无GUI模式下，安装成功。

但是，当我尝试从 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[..]
4

1 回答 1

0

该问题在邮件列表中被重复问过，并由 Claude Marché回答：

目录 examples-c/ 中的示例为什么是使用 Caduceus 语法的旧示例，这是 Frama-C 的一种前身。

最新的示例可以在目录 tests/c/ 中找到，也可以在其他几个地方找到，例如“ACSL by examples”等。

于 2014-10-08T07:36:17.207 回答