Habemus Frama-C in Fenestris (Frama-C on Windows, with WSL)

We have successfully compiled and tested the beta release of Frama-C 19 (Potassium) in the WSL (Windows Subsystem for Linux), using Debian. Installation is not trivial, especially for the graphical interface, but in the future this should provide a more robust way to run Frama-C on Windows, than relying on Cygwin/MinGW.

WSL + Cygwin/X

In a future post, or if there are explicit demands about the details of the installation procedure (for instance, via the frama-c-discuss mailing list), we may detail the whole process.

The main objective of this post is to (1) confirm to potential users that it is possible to install and run Frama-C using the Windows Subsystem for Linux and opam, and (2) inform that the WSL is likely a more efficient and robust solution than installing Cygwin and then opam on Windows from there. In our tests¹, WSL was faster to compile Frama-C and its dependencies, and required less workarounds. The major pain point was the graphical interface (which required the installation of a separate X server), but after the initial setup, the GUI seemed to run smoothly.

¹ None of the main Frama-C developers currently use Windows. What we could measure is that, between Cygwin on a Windows VM, and WSL on a Windows VM, the latter is much faster. We believe this remains true when running Windows natively.

Overview of the installation procedure

We used a Windows 10 Professional for the test. After enabling WSL, we installed Debian via the Windows Store, then some essential packages via apt (m4, curl, bzip2, and a few others), and installed opam 2 using the procedure based on curl. Note that using the opam package from Debian does not work, since it corresponds to opam 1.2. An upcoming Debian release will likely include opam 2, simplifying the procedure.

After installing opam 2 and configuring it without sandboxing (e.g. opam init --disable-sandboxing), which does not work on WSL, we installed a suitable OCaml compiler (4.07.1). We pinned the latest Frama-C Github release as indicated in the beta release e-mail:

opam pin add frama-c "https://github.com/Frama-C/Frama-C-snapshot.git#latest"

Then, we installed depext and ran opam depext frama-c, to get all of its dependencies. After installing a few more Debian packages and then opam packages, Frama-C was installed and could be run using the command line.

Graphical apps on WSL require some effort

Frama-C without its GUI is only half the fun. In order to get frama-c-gui fully working, we had to install an X server, since WSL does not currently provide one. One such server is Cygwin/X, which requires installing Cygwin and then a few packages such as xorg-server and xinit. Instructions are available with helpful screenshots, but for those not used to Cygwin, the procedure is somewhat cumbersome.

In our tests, we used SSH with X forwarding enabled (installing openssh-server and configuring /etc/ssh/sshd_config), then ran the XWin Server shortcut created by Cygwin/X, opening an xterm, connecting via SSH (with -Y) to the WSL Debian instance, and running frama-c-gui from there. This step definitely needs some polishing for a simpler installation procedure. But, for now, it suffices to know that it is possible to use the Frama-C GUI in Windows.

Conclusion

WSL is a good alternative for those wanting to try Frama-C on a Windows installation. A Linux virtual machine is still a more robust and accessible solution, which works with older versions of Windows, but for a more lightweight and performant experience, WSL already allows using Frama-C.

Contact us or send a message to frama-c-discuss if you would like more detailed instructions about installing Frama-C with WSL.