Bug#963705: frama-c-base: missing dependency why3
Package: frama-c-base
Version: 20191204+calcium-0.1
The package frama-c-base is not currently usable: when running `frama-c` (with or without arguments), we get the following message:
[kernel] User Error: [findlib] package 'why3' not found (required by `frama-c-wp')
This prevents Frama-C from working as intended (WP is one of the major tools in the Frama-C platform).
This happens because, starting from the Calcium version of Frama-C, the external tool Why3 is a mandatory requirement (it used to be optional). However, the frama-c-base package does not list why3 in its requirements.
It is possible to compile Frama-C without Why3, since it is dynamically loaded, which may explain why the issue was not detected.
Unfortunately, the Calcium release of Frama-C is incompatible with the why3 package available in Debian (1.3.1-2). Frama-C Calcium requires Why3 1.2.x.
If Why3 1.3.x is installed, then the following error happens when running `frama-c` Calcium:
[kernel] User Error: cannot load plug-in 'frama-c-wp': cannot load module
Details: error loading shared library: Dynlink error: error loading shared library: Failure("/usr/lib/frama-c/plugins/top/Wp.cmxs: undefined symbol: camlWhy3__Trans__seq_303")
Fortunately, the latest Frama-C release (21.0 - Scandium, released in June 2020) does work with Why3 1.3.1, so it should be possible to update the frama-c-base package to fix the issue.
I've never done Debian packaging, but I would like to help the maintainer(s) ot the frama-c-base package to update it if possible, so that Debian users can benefit from more recent Frama-C versions.
I use a Fedora myself, but a user reported installing the frama-c-base package with "Debian unstable", and I reproduced his results using the Docker `debian:unstable` image. /etc/issue reports "Debian GNU/Linux bullseye/sid".
--
André Maroneze
Researcher/Engineer CEA/List
Software Reliability and Security Laboratory
Reply to: