TL;DR: How do you guys use the WP plugin? (what front-ends, build tools, etc. do you use? What's your workflow?)
Frama-C ships with frama-c-gui, a GUI that helps developers navigate and analyze code and use Frama-C's many plugins. However, as justified in this article, it is in need of replacement. Ivette is being developed to replace it. However, it (currently) does not support WP.
Questions:
- Is there a front-end (besides
frama-c-guifor analyzing C code with the WP plugin for Frama-C? (plugins for vscode, emacs, etc.). If no: - Why not? (people actually use
frama-c-gui? Or their homebrew Makefile-s that "just work"? What do those look like?)
In summary: How do you guys use the WP plugin? (what front-ends, build tools, etc. do you use? What's your workflow?)
(Note: This question was posed in October 2023; answers will likely become opsolete in a few months/years)
The upcoming Frama-C version provides a minimal GUI for WP. Basically, it lists goals and provides a few filters to see the verification conditions per functions or properties.
No.
The reason why Ivette is currently incomplete is mainly a matter of manpower. The reason why there is no plug-ins for vscode, emacs or other environments is also a matter of manpower, plus the fact that the Frama-C team prefers investing effort on Ivette so that it is fully usable before pushing effort on other environments.
Most Frama-C users are on Linux, thus using the GTK3 GUI is still an option for them and while it is not the best experience one can have with verification, it still works. Thus, most of the time, the idea is:
frama-c-guiand see what fails, maybe use the integrated interactive prover,