Bug#959599: frama-c: FTBFS fixed upstream

[Andre Maroneze]

On Sat, 06 Jun 2020 09:47:57 -0400 John Scott  wrote:
> Control: forwarded -1 
https://lists.gforge.inria.fr/pipermail/frama-c-discuss/2020-June/005823.html

> Control: tags -1 fixed-upstream
>
> I'm having trouble finding their VCS and what commit fixed this, but 
updating
> Frama-C to the beta should be sufficient. Unstable and testing 
already have

> Why3 >= 1.3.

For information, the Frama-C public VCS (git) is available at: 
https://git.frama-c.com/pub/frama-c/-/tree/master


There is no specific commit which updated compatibility from Why3 1.2 to 
Why3 1.3 (there is an entire branch with several commits related to it), 
but https://git.frama-c.com/pub/frama-c/-/commit/1c7acc37c44f914f60a27 
would be close.


In any case, thanks for looking into this, and please tell us if there's 
anything we can do to help fix the frama-c package on Debian testing.


--
André Maroneze, for the Frama-C team

Bug#963705: frama-c-base: missing dependency why3

[Andre Maroneze]

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