--- layout: fc_discuss_archives title: Message 21 from Frama-C-discuss on September 2014 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] [Why3-club] Using Why3 api in frama-c plugin



Ah, that should be the issue. Thank you for all of your inputs.

Cheers,
Jos? Pinheiro

2014-09-05 22:54 GMT+01:00 Virgile Prevosto <virgile.prevosto at m4x.org>:

> Hello,
>
> Le ven. 05 sept. 2014 21:41:39 CEST,
> Jos? Pinheiro <7jpinheiro at gmail.com> a ?crit :
>
> > Yes, i checked they are correctly installed and i also tested using
> > the $(shell frama-c -print-lib-path) and  $(shell frama-c
> > -print-share-path) accordingly.
> >
> > I was able to fix the error, by opening on the source code of the
> > plugin both the modules Plugin and Printer.  For some reason this two
> > modules now require that i explicitly open them in the source code,
> > all the other modules are working normally without the need to
> > explicit opening them in the source code.
> >
>
> The issue is very probably that Why3 also has modules called Plugin and
> Printer, a situation which confuses OCaml when it is asked to search
> for .cmi in both Why3 and Frama-C library directories. There's little
> that can be done short of renaming or packing the files (in particular,
> I wouldn't bet that your fix will work consistently across various
> OCaml versions).
>
> Best regards,
> --
> E tutto per oggi, a la prossima volta.
> Virgile
>
> _______________________________________________
> 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
>



-- 
Cumprimentos,
Jos? Pinheiro
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20140908/ae84656a/attachment.html>