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] installing Jessie plug-in




As Pascal said, if you don't compile Jessie with the OCaml provided by 
that Frama-C package, it won't work.

I'm surprised that ocamlgraph is not included in that Frama-C package, 
because Frama-C needs ocamlgraph. May be the problem is just that the 
configure script of Jessie does not find the ocamlgraph library at the 
right place. Could send the output of the ./configure script (of course 
after adding in your PATH the path to the ocaml binary provided by 
Frama-C) ?

- Claude


Le 08/04/2013 16:09, Stephen Siegel a ?crit :
> I used OCaml 4.00.1 (installed via MacPorts) to compile Why:
>
> plugins$ ocaml -version
> The OCaml toplevel, version 4.00.1
> plugins$ which ocaml
> /opt/local/bin/ocaml
>
> The only reason I didn't use the binary in the Mac OS X Frama-C package
> is that it did not include ocamlgraph, required for Why.  (I also got
> ocamlgraph from Macports: sudo port install ocaml-ocamlgraph)
>
>> Could you double-check that the Jessie.cmxs file in Frama-C plugins directory is not an old version ?
>
> I don't know how to do this: it's a binary file.
>
> -s
>
>
> On Apr 8, 2013, at 3:42 AM, Pascal Cuoq <pascal.cuoq at gmail.com
> <mailto:pascal.cuoq at gmail.com>> wrote:
>
>>     On 04/08/2013 05:17 AM, Stephen Siegel wrote:
>>
>>         I've run into some problems installing the Jessie plugin on OS
>>         X 10.8.3, with Frama-C Oxygen.
>>
>> On Mon, Apr 8, 2013 at 6:47 AM, Claude Marche <Claude.Marche at inria.fr
>> <mailto:Claude.Marche at inria.fr>> wrote:
>>
>>     This is the typical message displayed when trying to load a
>>     plug-in that was compiled with a different OCaml version than the
>>     one used to compile Frama-C. Could you double-check that the
>>     Jessie.cmxs file in Frama-C plugins directory is not an old version ?
>>
>>
>> Note that the reason I mentioned the OCaml compiler in the binary Mac
>> OS X Frama-C package is that there is no object-level compatibility at
>> all between OCaml versions. In order to compile and link a plug-in
>> with the Frama-C from the binary package, one must use OCaml 4.00.1
>> (the version that was used to compile the Frama-C kernel in that package).
>>
>> One such compiler is provided in the package (at
>> /usr/local/Frama-C/ocaml-4.00.1p/bin ).
>>
>> I am going to try and install the Jessie plug-in from Why 2.32 on top
>> of the Frama-C OS X binary package as soon as I have time for it, and
>> I will report on the difficulties I meet.
>> _______________________________________________
>> Frama-c-discuss mailing list
>> Frama-c-discuss at lists.gforge.inria.fr
>> <mailto:Frama-c-discuss at lists.gforge.inria.fr>
>> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss
>
>
>
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss
>

-- 
Claude March?                          | tel: +33 1 72 92 59 69
INRIA Saclay - ?le-de-France           |
Universit? Paris-sud, Bat. 650         | http://www.lri.fr/~marche/
F-91405 ORSAY Cedex                    |