--- layout: fc_discuss_archives title: Message 21 from Frama-C-discuss on August 2017 ---
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>> 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>> 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> >>>> 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 | >>> _______________________________________________ >>> Why-discuss mailing list >>> 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/ F-91405 ORSAY Cedex |