Frama-C-discuss mailing list archives

Claude.Marche at inria.fr (Claude Marché) · Tue, 22 Aug 2017 10:09:21 +0200

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                    |

Frama-C-discuss mailing list archives

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