--- layout: fc_discuss_archives title: Message 22 from Frama-C-discuss on September 2014 ---
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 >