Source: why3, frama-c Control: found -1 why3/1.5.0-1 Control: found -1 frama-c/20211203-chromium-1 Severity: serious Tags: sid bookworm User: debian-ci@lists.debian.org Usertags: breaks needs-update Dear maintainer(s),With a recent upload of why3 the autopkgtest of frama-c fails in testing when that autopkgtest is run with the binary packages of why3 from unstable. It passes when run with only packages from testing. In tabular form:
pass fail
why3 from testing 1.5.0-1
frama-c from testing 20211203-chromium-1
all others from testing from testing
I copied some of the output at the bottom of this report.
Currently this regression is blocking the migration of why3 to testing
[1]. Due to the nature of this issue, I filed this bug report against
both packages. Can you please investigate the situation and reassign the
bug to the right package?
More information about this bug and the reason for filing it can be found on https://wiki.debian.org/ContinuousIntegration/RegressionEmailInformation Paul [1] https://qa.debian.org/excuses.php?package=why3 https://ci.debian.net/data/autopkgtest/testing/amd64/f/frama-c/21530048/log.gz [kernel] User Error: cannot load plug-in 'frama-c-wp': cannot load moduleDetails: error loading shared library: Dynlink error: error loading shared library: Failure("/usr/lib/frama-c/plugins/top/Wp.cmxs: undefined symbol: camlWhy3__Env__fun_3995") [kernel] User Error: Deferred error message was emitted during execution. See above messages for more information.
[kernel] Frama-C aborted: invalid user input. autopkgtest [05:10:25]: test eva
Attachment:
OpenPGP_signature
Description: OpenPGP digital signature