--- layout: fc_discuss_archives title: Message 23 from Frama-C-discuss on August 2017 ---
Le 22/08/2017 10:09, Claude Marché a écrit : >> There is an unresolved issue. To use the Jessie plugin, I installed why >> 2.38 on both Ubuntu and MacOS. It works well on Ubuntu, but on MacOS, >> Frama-C cannot locate the Jessie plugin. Do you have any thought on this? > > I hope that someone on the Frama-C list could suggest a procedure to > investigate that failure. Something using options --kernel-debug, > --plugin-path, to expose why dynamic loading of Jessie.cmxs fails. In order to get the exact failure when loading Jessie.cmxs, you can run Frama-C as follows: $ frama-c -kernel-msg-key dynling <other options and files> Best, Julien >>> On Aug 22, 2017, at 3:52 AM, Claude Marché <Claude.Marche at inria.fr >>> <mailto:Claude.Marche at inria.fr>> wrote: >>> >>> >>> Hi to all, >>> >>> I forward this message from the Why list to the Frama-C list, in case >>> one has an answer. >>> >>> It seems that the compilation of the Jessie plugin fails because some >>> strange interaction with the PathCrawler plugin. The log says: >>> >>> # make -C frama-c-plugin depend >>> # make[1]: Entering directory >>> '/home/park11/.opam/4.03.0/build/why.2.38/frama-c-plugin' >>> # make[1]: Leaving directory >>> '/home/park11/.opam/4.03.0/build/why.2.38/frama-c-plugin' >>> # Makefile:684: recipe for target '.depend' failed >>> ### stderr ### >>> # 1 shift/reduce conflict. >>> # Makefile:117: /home/park11/PathCrawler/Makefile.dynamic: No such file >>> or directory >>> # make[1]: *** No rule to make target >>> '/home/park11/PathCrawler/Makefile.dynamic'. Stop. >>> # make: *** [.depend] Error 2 >>> >>> Any thought ? >>> >>> A poor suggestion: deactivate/suppress the PathCrawler plugin to compile >>> Jessie, then reactivate/reinstall it afterwards >>> >>> - Claude >>> >>> Le 14/08/2017 à 22:45, Junkil Park a écrit : >>>> Hi, >>>> >>>> As I posted in my previous email, I had a problem with installing Jessie >>>> (why.2.38) on my Mac through opam. I still didn't resolve it. If anyone >>>> can help, I would appreciate it. >>>> >>>> This time, I try to install why 2.38 through opam (Ocaml v 4.03.0) on my >>>> Ubuntu machine (16.04). But, it failed with the following error message: >>>> >>>> The following actions will be performed: >>>> â install why 2.38 >>>> >>>> =-=- Gathering sources >>>> =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= >>>> [why] Archive in cache >>>> >>>> =-=- Processing actions >>>> -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= >>>> [ERROR] The compilation of why failed at "make". >>>> Processing 1/1: [why: rm] >>>> #=== ERROR while installing why.2.38 >>>> ==========================================# >>>> # opam-version 1.2.2 >>>> # os linux >>>> # command make >>>> # path /home/park11/.opam/4.03.0/build/why.2.38 >>>> # compiler 4.03.0 >>>> # exit-code 2 >>>> # env-file >>>> /home/park11/.opam/4.03.0/build/why.2.38/why-32328-d2c37b.env >>>> # stdout-file >>>> /home/park11/.opam/4.03.0/build/why.2.38/why-32328-d2c37b.out >>>> # stderr-file >>>> /home/park11/.opam/4.03.0/build/why.2.38/why-32328-d2c37b.err >>>> ### stdout ### >>>> # [...] >>>> # printf "option=\"-R /home/park11/.opam/4.03.0/lib/why/coq Why\"\n" >> >>>> lib/why3/why3.conf >>>> # printf "\n" >> lib/why3/why3.conf >>>> # printf "[editor_modifiers proofgeneral-coq]\n" >> lib/why3/why3.conf >>>> # printf "option=\"--eval \\\\\"(setq coq-load-path (cons >>>> '(\\\\\\\\\\\\\"/home/park11/.opam/4.03.0/lib/why/coq\\\\\\\\\\\\\" >>>> \\\\\\\\\\\\\"Why\\\\\\\\\\\\\") coq-load-path))\\\\\"\"\n" >> >>>> lib/why3/why3.conf >>>> # rm -f .depend >>>> # ocamldep.opt -slash -I src -I jc -I java -I mix -I tools src/*.ml >>>> src/*.mli jc/*.mli jc/*.ml java/*.mli java/*.ml mix/*.mli mix/*.ml > >>>> .depend >>>> # make -C frama-c-plugin depend >>>> # make[1]: Entering directory >>>> '/home/park11/.opam/4.03.0/build/why.2.38/frama-c-plugin' >>>> # make[1]: Leaving directory >>>> '/home/park11/.opam/4.03.0/build/why.2.38/frama-c-plugin' >>>> # Makefile:684: recipe for target '.depend' failed >>>> ### stderr ### >>>> # 1 shift/reduce conflict. >>>> # Makefile:117: /home/park11/PathCrawler/Makefile.dynamic: No such file >>>> or directory >>>> # make[1]: *** No rule to make target >>>> '/home/park11/PathCrawler/Makefile.dynamic'. Stop. >>>> # make: *** [.depend] Error 2 >>>> >>>> >>>> >>>> =-=- Error report >>>> -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= >>>> The following actions failed >>>> â install why 2.38 >>>> No changes have been performed >>>> >>>> >>>> Thanks, >>>> Junkil >>>> >>>> >>>>> On Aug 14, 2017, at 4:45 PM, Junkil Park <park11 at seas.upenn.edu >>>>> <mailto:park11 at seas.upenn.edu> >>>>> <mailto:park11 at seas.upenn.edu>> wrote: >>>>> >>>>> Hi, >>>>> >>>>> Thank you for your answer, Claude. >>>>> >>>>> First of all, the installation completed without error: >>>>> =-=- Processing actions >>>>> -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= ð« >>>>> â installed why3-base.0.87.3 >>>>> â installed why3.0.87.3 >>>>> â installed frama-c-base.20161101 >>>>> â installed frama-c.20161101 >>>>> â installed why.2.38 >>>>> Done. >>>>> >>>>> >>>>> Secondly, it seems that frama-c has options neither '-plugin-path' or >>>>> '-kernel-debug'. Instead, the 'plugins' option of frama-c shows the >>>>> list of plugins, which does not include Jessie. These are the only >>>>> files which name contain the keyword 'Jessie' in my opam system: >>>>> ~/.opam/4.05.0/bin/jessie >>>>> ~/.opam/4.05.0/bin/jessie.log >>>>> ~/.opam/4.05.0/lib/why/why3/jessie_why3.mlw >>>>> ~/.opam/4.05.0/lib/why/why3/jessie_why3theories.why >>>>> >>>>> >>>>> Lastly, I downloaded and unzip the source code of Why >>>>> from http://why.lri.fr/download/why-2.38.tar.gz, which contains the >>>>> folder 'frama-c-plugin'. However, I cannot find the 'frama-c-plugin' >>>>> folder and its files in my opam installation. Can this be a problem? >>>>> >>>>> BTW, I am doing this on my Mac. >>>>> >>>>> Thanks, >>>>> Junkil >>>>> >>>>>> On Aug 3, 2017, at 3:12 AM, Claude Marché <Claude.Marche at inria.fr >>>>>> <mailto:Claude.Marche at inria.fr> >>>>>> <mailto:Claude.Marche at inria.fr>> wrote: >>>>>> >>>>>> >>>>>> Hi, >>>>>> >>>>>> Indeed 'opam install why' should do everything fine in one shot. You're >>>>>> not missing anything, so you should check whether installation went >>>>>> without error. >>>>>> >>>>>> To investigate the problem, you should check whether the plugin >>>>>> code is >>>>>> at the right place, that is some Jessie.cmxs present in the `frama-c >>>>>> -plugin-path` Also option -kernel-debug might help. >>>>>> >>>>>> You should also consider asking for help on the Frama-C discuss list >>>>>> >>>>>> - Claude >>>>>> >>>>>> >>>>>> >>>>>> Le 31/07/2017 à 20:48, Junkil Park a écrit : >>>>>>> Hi, >>>>>>> >>>>>>> To use the Jessie plugin of Frama-C, I installed >>>>>>> Frama-C(Silicon-20161101), Why(2.38), Why3(0.87.3) through opam >>>>>>> (ocaml v. 4.05.0). >>>>>>> >>>>>>> However, Frama-C cannot find the Jessie plugin, saying >>>>>>> >>>>>>> [kernel] user error: option `-jessie' is unknown. >>>>>>> >>>>>>> How can I enable the Jessie plugin? Am I missing something? >>>>>>> >>>>>>> Thanks, >>>>>>> Junkil >>>>>>> _______________________________________________ >>>>>>> Why-discuss mailing list >>>>>>> Why-discuss at lists.gforge.inria.fr >>>>>>> <mailto:Why-discuss at lists.gforge.inria.fr> >>>>>>> <mailto:Why-discuss at lists.gforge.inria.fr> >>>>>>> https://lists.gforge.inria.fr/mailman/listinfo/why-discuss >>>>>>> >>>>>> >>>>>> -- >>>>>> Claude Marché | tel: +33 1 69 15 66 08 >>>>>> INRIA Saclay - Ãle-de-France | >>>>>> Université Paris-sud, Bat. 650 | http://www.lri.fr/~marche/ >>>>>> <http://www.lri.fr/%7Emarche/> >>>>>> <http://www.lri.fr/%7Emarche/> >>>>>> F-91405 ORSAY Cedex | >>>>>> _______________________________________________ >>>>>> Why-discuss mailing list >>>>>> Why-discuss at lists.gforge.inria.fr >>>>>> <mailto:Why-discuss at lists.gforge.inria.fr> >>>>>> <mailto:Why-discuss at lists.gforge.inria.fr> >>>>>> https://lists.gforge.inria.fr/mailman/listinfo/why-discuss >>>>> >>>> >>> >>> -- >>> Claude Marché | tel: +33 1 69 15 66 08 >>> INRIA Saclay - Ãle-de-France | >>> Université Paris-sud, Bat. 650 | http://www.lri.fr/~marche/ >>> <http://www.lri.fr/%7Emarche/> >>> F-91405 ORSAY Cedex | >> >