--- Begin Message ---
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
--- End Message ---
--- Begin Message ---
Source: frama-c
Source-Version: 20200625+scandium-1
Done: Ralf Treinen <treinen@debian.org>
We believe that the bug you reported is fixed in the latest version of
frama-c, which is due to be installed in the Debian FTP archive.
A summary of the changes between this version and the previous one is
attached.
Thank you for reporting the bug, which will now be closed. If you
have further comments please address them to 963705@bugs.debian.org,
and the maintainer will reopen the bug report if appropriate.
Debian distribution maintenance software
pp.
Ralf Treinen <treinen@debian.org> (supplier of updated frama-c package)
(This message was generated automatically at their request; if you
believe that there is a problem with it please contact the archive
administrators by mailing ftpmaster@ftp-master.debian.org)
-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA256
Format: 1.8
Date: Tue, 25 Aug 2020 20:37:33 +0200
Source: frama-c
Architecture: source
Version: 20200625+scandium-1
Distribution: unstable
Urgency: medium
Maintainer: Debian OCaml Maintainers <debian-ocaml-maint@lists.debian.org>
Changed-By: Ralf Treinen <treinen@debian.org>
Closes: 959599 963705
Changes:
frama-c (20200625+scandium-1) unstable; urgency=medium
.
* New upstream release.
This version works with why3 1.3.1 (closes: #963705)
This version solves FTBFS (closes: #959599)
* Add myself as uploader
* Add dependency on ${perl:Depends} and dependency on python3
* Build-dependencies:
- use debhelper-compat, remove file debian/compat
- bump versions according to upstream's opam file
- drop ocaml-best-compilers which is now a virtual package
- add liblablgtk{sourceview}3-ocaml-dev
* Debhelper-compatibility level 13
- invoke dh --without autoreconf
* Installation:
- install the complete directory /usr/lib/frama-c/plugins
- install usr/lib/libeacsl-dlmalloc.a
- install frama-c-script and frama-c-gui binaries
- register ptests and e-acsl-gcc as not installed
* Add symbolic link for the manpage of frama-c-gui.byte
* d/copyright:
- remove entries concerning files that are no longer in the source tree.
- add text of the BSD-3 license, rename to BSD-3-clause
- migrate to machine-readable format 1.0
- remove copy of LGPL 2.1
* Fix format of long description
* Standards-Version 4.5.0
* Update Homepage
Checksums-Sha1:
e5b49760965da248df40d2415ba604fb232f0f1b 2290 frama-c_20200625+scandium-1.dsc
f3c1a40ba54ace7eb33ddb9f53fcf4d6f92a9a54 6381637 frama-c_20200625+scandium.orig.tar.gz
476ebfafaf4e691d21c13033bcfa90028a9bcd1e 14952 frama-c_20200625+scandium-1.debian.tar.xz
188dd3a8b356f014a9b723524627947ffaf5e5f4 15274 frama-c_20200625+scandium-1_source.buildinfo
Checksums-Sha256:
497005b57fb9aaa0d19ae4e5ce516ad1332e012f5854645b64325660df468fc4 2290 frama-c_20200625+scandium-1.dsc
74c23ac34c97d2d266b8f3e62dd73fd5367058439ddba266a42c850103337507 6381637 frama-c_20200625+scandium.orig.tar.gz
ac1e418639f6e040e4f5929f011deaff69337134a58cca2edcd1469fb5843024 14952 frama-c_20200625+scandium-1.debian.tar.xz
f7d3a6e92f473ef312711cf2d9d861778c56d882337cd9fcf0abf5b27a92d3ed 15274 frama-c_20200625+scandium-1_source.buildinfo
Files:
541f54c0d98164b5f76003948fb05435 2290 devel optional frama-c_20200625+scandium-1.dsc
2cfbcbc1d1121fb3b624577a15882aa5 6381637 devel optional frama-c_20200625+scandium.orig.tar.gz
a787044b32dca3c7b49e56b17128d95f 14952 devel optional frama-c_20200625+scandium-1.debian.tar.xz
9d1c395db58c9cf73f256a20f91727ae 15274 devel optional frama-c_20200625+scandium-1_source.buildinfo
-----BEGIN PGP SIGNATURE-----
iQIzBAEBCAAdFiEEAgVIKeEtDyqOZI5idFxHZtTKzf8FAl9FY1MACgkQdFxHZtTK
zf9xEw//Sc+FI4jCMSZJIudlP64JNIEZrYbDpUNaacXvH6lWfWq5pZvCyuKJGipB
mUrFucs2/q6PXM4svQ5Vl3U2c8os6fHSrLKKBRN0f19+h2+GTs8JkO718Le1dfxB
arIIEpkSyt68jEOpfqYwqp2pOJe3BxFe/l7sohhNmQh5DtCQOlrk6qHQ8HdmEx3/
NHcdMwft8K+IW5OHJCISNc/RJe0rMTIHli/T9rj7w2DeklHXnIEuXKsWhyUDp/hF
JYQryGo0yJCwJXt6qSTMTk/1R6JbHaVFvTaW4r0xvQZOKHfy5OAy6ZAaz7RRuUEC
GXNOTwN37ATgjK3rXIuy4Y6aVBzTeHt9eEnt16mr9S1iJEZcW/kGD78X9bh/icrb
aU6fsCzlqCRhb6tRX44FdGKt8X6VifRokGhFT/tNIG4ZfONsnWZU0rrqqzch/+G9
OoP8QDCKGy857Fe9R0S4xqvjIPVElFvx6jqD+JWP1paAo0JdAwGdlrx7wr64mZe0
NHbfUYx63xlIUvRY/Jns+O8I55aZb0CGcenr68Ra2AFOV5wS+RXWW1NJzWdWPUtm
4ZIjesKoGwQ4EnznfNeudzSjvoN687P8ZnwgJzPkIYrszEBdSYNj0m7JjZ2JG5yM
QS8/KWY71UfSSZzst99ZTOp2Kv5sRRR5tEZraW5BQWIeayg4VQw=
=sKXi
-----END PGP SIGNATURE-----
--- End Message ---