--- layout: fc_discuss_archives title: Message 10 from Frama-C-discuss on April 2013 ---
[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                    |