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