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

Question

我正在尝试从 Allan Blanchard 的 tutorial 学习 frama-c我在按照教程中的建议验证安装时遇到了麻烦。作者提供了C file带有 ACSL 注释，所有这些 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支持。如 reference configuration 中所述对于 Frama-C，已知完全支持 Alt-Ergo 2.2.0，因此您可能需要 opam pin add alt-ergo 2.2.0使用该版本。之后别忘了让Why3重新检测证明者why3 config --detect-provers .如果这一步有问题，请随时就该特定主题提出一个新问题(尽管我怀疑该问题与 Alt-Ergo 2.4.0 相关)。