Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

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