--- layout: fc_discuss_archives title: Message 22 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



I don't think this could be the reason. The Why3 library packs all its 
Ocaml modules into a main module called "Why3", so no name conflicts 
should occur.

I recommend that you set

VERBOSEMAKE=yes

in your Makefile, and send us the exact command line that generates a 
compilation error.

By the way, I have a possible explanation, because I faced that issue: 
with the last version 0.84 of Why3, if you enable the use of the camlzip 
library for file compression, then you may not be able to load the 
generated plug-in dynamically. In that case, a solution is to configure 
Why3 with option --disable-zip before its compilation.

- Claude

On 09/08/2014 05:07 PM, Jos? Pinheiro wrote:
> 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
> <mailto:virgile.prevosto at m4x.org>>:
>
>     Hello,
>
>     Le ven. 05 sept. 2014 21:41:39 CEST,
>     Jos? Pinheiro <7jpinheiro at gmail.com <mailto: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
>     <mailto:Frama-c-discuss at lists.gforge.inria.fr>
>     http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss
>
>
>
>
> --
> Cumprimentos,
> Jos? Pinheiro
>
>
> _______________________________________________
> 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
>