--- layout: fc_discuss_archives title: Message 22 from Frama-C-discuss on August 2017 ---
Le 22/08/2017 à 10:05, Junkil Park a écrit : > Hi Claude, > > Thank you for forwarding this. However, the issue was due to my setting > of the variable FRAMAC_SHARE to use some version of PathCrawler. So, I > fixed it. OK, good to know. > 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. - Claude > Thanks, > Junkil > >> 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 | > -- Claude Marché | tel: +33 1 69 15 66 08 INRIA Saclay - Ãle-de-France | Université Paris-sud, Bat. 650 | http://www.lri.fr/~marche/ F-91405 ORSAY Cedex |