GNU bug report logs - #38635
[WIP PATCH] Add why3 and frama-c

Previous Next

Full log

Message #11 received at 38635 <at> debbugs.gnu.org (full text, mbox):

From: Julien Lepiller <julien <at> lepiller.eu>
To: 38635 <at> debbugs.gnu.org
Subject: [WIP PATCH v2] Add why3 and frama-c
Date: Wed, 2 Sep 2020 15:05:30 +0200

[Message part 1 (text/plain, inline)]

Hi Guix!

I've updated my patches to the newest versions of why3 and frama-c. The
issue is still present as before:

$ frama-c --help

[kernel] User Error: cannot load plug-in 'zip': cannot load module
  Details: error loading shared library: Dynlink.Error
(Dynlink.Cannot_open_dll
"Failure(\"/gnu/store/jrbkl0ls1vqnr1w7gcbg8jlxcd1jp71m-profile/lib/ocaml/site-lib/zip/zip.cmxa:
invalid ELF header\")") [kernel] User Error: cannot load plug-in
'why3': cannot load module Details: error loading shared library:
Dynlink.Error (Dynlink.Cannot_open_dll
"Failure(\"/gnu/store/jrbkl0ls1vqnr1w7gcbg8jlxcd1jp71m-profile/lib/ocaml/site-lib/why3/why3.cmxs:
undefined symbol: camlGzip\")") [kernel] User Error: cannot load
plug-in 'frama-c-wp': cannot load module Details: error loading shared
library: Dynlink.Error (Dynlink.Cannot_open_dll
"Failure(\"/gnu/store/bicyz7li6bvrxh4kh2h1dc5398bx5xsm-frama-c-21.1/lib/frama-c/plugins/top/Wp.cmxs:
undefined symbol: camlWhy3__Theory\")") [kernel] User Error: Deferred
error message was emitted during execution. See above messages for more
information. [kernel] Frama-C aborted: invalid user input.

[0001-gnu-Add-why3.patch (text/x-patch, attachment)]

[0002-gnu-Add-frama-c.patch (text/x-patch, attachment)]

Previous Next

GNU bug tracking system
Copyright (C) 1999 Darren O. Benham, 1997,2003 nCipher Corporation Ltd, 1994-97 Ian Jackson.