--- layout: fc_discuss_archives title: Message 23 from Frama-C-discuss on August 2017 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] [Why-discuss] Installing Jessie



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                    |
>>
>