Description of problem: After I install frama-c and why-jessie, I get this error: $ frama-c -jessie [kernel] warning: cannot load plug-in `Jessie' (incompatible with Neon-20140301). [kernel] user error: option `-jessie' is unknown. use `frama-c -help' for more information. [kernel] Frama-C aborted: invalid user input. However, the upstream site (http://krakatoa.lri.fr/#overview) says that it should work with frama-c Neon and why 2.34, which I have. Version-Release number of selected component (if applicable): $ rpm -q frama-c frama-c-1.10-5.fc20.x86_64 $ rpm -q why-jessie why-jessie-2.34-5.fc20.x86_64 How reproducible: Always. Steps to Reproduce: 1. Install frama-c and why-jessie on F20 x86_64. 2. Run "frama-c -jessie" 3. Observe the above error. :-( Actual results: The above error is displayed. Expected results: I think this combination of versions is supposed to work fine. Additional info: To be honest, I'm not quite sure if this is an upstream bug or a packaging bug, but I figured that filing this is a good first attempt at making progress. If this is an upstream issue, let me know and I am happy to re-file it there.
$ frama-c -verbose 2 -jessie [kernel] warning: cannot load plug-in `Jessie' (incompatible with Neon-20140301). The exact failure is: error loading shared library: /usr/lib64/frama-c/plugins/Jessie.cmxs: undefined symbol: camlStream. [kernel] user error: option `-jessie' is unknown. use `frama-c -help' for more information. [kernel] Frama-C aborted: invalid user input. I'm not sure why camlStream is undefined. I will look into it.
I see that camlStream is an undefined symbol in %{_libdir}/ocaml/stdlib.a, which is where the plugin is picking it up, apparently. I don't believe the plugin actually needs this symbol; at least, I do not see any instances of Stream in the source code. I don't know whether this means that Jessie is being linked incorrectly somehow (maybe a critical link flag is missing?), or if this is an ocaml bug. I will ask the ocaml maintainer to weigh in on this.
(In reply to Jerry James from comment #2) > I see that camlStream is an undefined symbol in %{_libdir}/ocaml/stdlib.a, > which is where the plugin is picking it up, apparently. I don't believe the > plugin actually needs this symbol; at least, I do not see any instances of > Stream in the source code. I don't know whether this means that Jessie is > being linked incorrectly somehow (maybe a critical link flag is missing?), > or if this is an ocaml bug. I will ask the ocaml maintainer to weigh in on > this. I think the first thing to say is that a module called "Stream" containing a function named "Stream.peek" will cause the compiler to generate a symbol called "camlStream__peek_NNN" (where NNN is a serial number because OCaml allows multiple functions to have the same name). The module itself will generate a data symbol "camlStream". However I'm not sure what this is used for. stdlib.a in the compiler has camlStream defined: $ nm /usr/lib64/ocaml/stdlib.a | grep 'camlStream$' 0000000000000008 D camlStream U camlStream $ rpm -qf /usr/lib64/ocaml/stdlib.a ocaml-4.01.0-14.fc21.x86_64 The additional complexity here is with .cmxs files, dynamically loaded shared libraries. I don't know a lot about how these work, but I assume they cannot use the stdlib.a file, but must use some kind of shared library. I don't see any shared library that corresponds to stdlib, but if that was really missing, nothing would work at all. I suggest asking upstream.
Another thing: does it work with Fedora Rawhide? The version of OCaml in Rawhide is signficantly newer and better. I don't use the F20 OCaml any more. I just install the Rawhide packages on F20.
Thanks for the input, Richard. (In reply to Richard W.M. Jones from comment #4) > Another thing: does it work with Fedora Rawhide? The version of OCaml > in Rawhide is signficantly newer and better. I don't use the F20 > OCaml any more. I just install the Rawhide packages on F20. The same problem manifests on both Rawhide and F20. I will ask upstream if they have any ideas.
why-2.34-5.fc20,frama-c-1.10-5.fc20,why3-0.83-6.fc20 has been submitted as an update for Fedora 20. https://admin.fedoraproject.org/updates/why-2.34-5.fc20,frama-c-1.10-5.fc20,why3-0.83-6.fc20
There were 3 bugs working together to kill the poor Jessie plugin. First, we attempted to add Fedora's linker flags to the Frama-C build, and accidentally overwrote the existing linker flags instead of adding to them. In particular, this wiped out -linkall, which is why the Stream implementation could not be found. Second, we linked Frama-C (and why and why3) with -Wl,-z,relro,-z,now and the ",-z,now" part seems to interfere with name resolution while loading plugins. Third, Frama-C and why both have a module named Project. After fixing the previous 2 bugs, attempting to load the Jessie plugin resulted in an error due to the conflicting modules with that name. The why build system actually builds project.ml with -for-pack Jc, and uses -pack when building jc.cmx, which is included in Jessie.cmxs. Therefore, the why module ought to be named Jc.Project, not Project, and the two should not conflict. That happens with ocaml 3.x, but not with ocaml 4.x. For some reason, with ocaml 4, the name is still just Project. I have put a workaround into place (renaming the why module to Whyproject), but this shouldn't be necessary. I don't yet know if this is a bug in ocaml 4, or if we need to do something different when compiling with ocaml 4 to get the results we got with ocaml 3.
Package why-2.34-5.fc20, frama-c-1.10-5.fc20, why3-0.83-6.fc20: * should fix your issue, * was pushed to the Fedora 20 testing repository, * should be available at your local mirror within two days. Update it with: # su -c 'yum update --enablerepo=updates-testing why-2.34-5.fc20 frama-c-1.10-5.fc20 why3-0.83-6.fc20' as soon as you are able to. Please go to the following url: https://admin.fedoraproject.org/updates/FEDORA-2014-7850/why-2.34-5.fc20,frama-c-1.10-5.fc20,why3-0.83-6.fc20 then log in and leave karma (feedback).
why-2.34-5.fc20, frama-c-1.10-5.fc20, why3-0.83-6.fc20 has been pushed to the Fedora 20 stable repository. If problems still persist, please make note of it in this bug report.
Hm, I still seem to be seeing this issue. :( ricky@t520 /tmp$ frama-c -verbose 2 -jessie [kernel] warning: cannot load plug-in `Jessie' (incompatible with Neon-20140301). The exact failure is: error loading shared library: /usr/lib64/frama-c/plugins/Jessie.cmxs: undefined symbol: camlStream. [kernel] user error: option `-jessie' is unknown. use `frama-c -help' for more information. [kernel] Frama-C aborted: invalid user input. ricky@t520 /tmp$ for i in ocaml frama-c why why3; do rpm -q $i; done ocaml-4.00.1-3.fc20.x86_64 frama-c-1.10-6.fc20.x86_64 why-2.34-6.fc20.x86_64 why3-0.83-6.fc20.x86_64
Where did you get these two? frama-c-1.10-6.fc20.x86_64 why-2.34-6.fc20.x86_64 The latest updates for Fedora 20 are -5 in both cases. I have not built nor pushed any -6 versions. And with the Fedora-built -5 versions, your example works for me.
Oh jeeze. I built it myself when I was trying to debug the initial issue, and because the release is higher than the current f20 package, I never got your update. Sorry for wasting your time! :-(
No problem. I manage to shoot myself in the foot on a fairly regular basis, so I know the feeling. :-)