Frama-C 的 IDE/工作流程？ （特别是对于 WP 插件）

Question

TL;DR：你们如何使用 WP 插件？ （你使用什么前端、构建工具等？你的工作流程是什么？）

Frama-C 附带

frama-c-gui

，这是一个 GUI，可帮助开发人员导航和分析代码并使用 Frama-C 的许多插件。然而，正如本文所证明的那样，它需要更换。 Ivette 正在开发中以取代它。但是，它（目前）不支持 WP。

问题：

1. 是否有前端（除了

   frama-c-gui

   用于使用 Frama-C 的 WP 插件分析 C 代码？（vscode、emacs 等插件）。如果没有：
2. 为什么不呢？ （人们实际上使用

   frama-c-gui

   ？或者他们的自制 Makefile-s 可以“正常工作”？那些看起来像什么？）

总结：你们如何使用WP插件？ （你使用什么前端、构建工具等？你的工作流程是什么？）

（注意：这个问题是在 2023 年 10 月提出的；答案可能会在几个月/几年内变得过时）

Answer 1

但是，它（目前）不支持 WP。

即将推出的 Frama-C 版本为 WP 提供了一个最小的 GUI。基本上，它列出了目标并提供了一些过滤器来查看每个函数或属性的验证条件。

是否有前端（除了 frama-c-gui 之外，还可以使用 Frama-C 的 WP 插件来分析 C 代码？（vscode、emacs 等插件）。

没有。

为什么不呢？ （人们实际上使用 frama-c-gui？或者他们的自制 Makefile-s 可以“正常工作”？那些看起来像什么？）

Ivette目前之所以不完善，主要是人手的问题。之所以没有针对 vscode、emacs 或其他环境的插件，也是人力问题，再加上 Frama-C 团队更喜欢在 Ivette 上投入精力，以便在其他环境上投入精力之前使其完全可用。

大多数 Frama-C 用户都使用 Linux，因此使用 GTK3 GUI 仍然是他们的一种选择，虽然这不是验证的最佳体验，但它仍然有效。因此，大多数时候，想法是：

• 在您最喜欢的编辑器中准备源代码，
• 启动

  frama-c-gui

  并查看失败的原因，也许可以使用集成的交互式证明器，
• 当需要更改源代码时，在编辑器中准备更改并重新启动 Frama-C。