Frama-c 无法证明 Allan Blanchard 教程中的 verify.c

Question

我正在尝试向 Allan Blanchard 的 tutorial 学习 frama-c，但我无法按照教程中的建议验证安装。作者提供了一个带有ACSL注解的C file，这些都是frama-c应该能够证明的。但是，当我运行命令 (frama-c-gui -wp -rte main.c) 时，我得到以下信息：

Frama-C GUI screenshot

我通过 opam（2.0.4 版）在 ocaml-base-compiler.4.11.1 开关上安装了 frama-c（22.0 版）。当我安装它时，我遇到了Why3 无法检测到 Alt-Ergo 的问题，我最终手动编辑了 ~/why3.config。尽管我不确定它是否与上述问题有关，但我在这里提到它。

Answer 1

从我可以根据屏幕截图判断，这似乎确实非常相关。值得注意的是，每当您在证明者后面看到 Failed 时，这表明出现了问题：证明者根本无法证明某事，而宁愿将其指示为 Unknown。

在您的情况下，我倾向于认为问题出在您使用的版本 Alt-Ergo 2.4.0 相当新（实际上比最新的 Why3 版本更新），并且Why3 尚不支持。正如在 Frama-C 的 reference configuration 中提到的，众所周知，Alt-Ergo 2.2.0 得到了完全支持，因此您可能希望 opam pin add alt-ergo 2.2.0 使用该版本。之后，不要忘记让Why3 重新检测证明者why3 config --detect-provers。如果此步骤有问题，请随时就该特定主题提出新问题（尽管我怀疑该问题与 Alt-Ergo 2.4.0 有关）。