--- layout: fc_discuss_archives title: Message 11 from Frama-C-discuss on July 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] How to compil Frama-C with an existing Why installation



Is there anyone who have already done so ? Because I have been
unsuccessful so far. Personally I don't need Why outside of Frama-C's
dependency so it doesn't blocking me or anything, but as a packager, I
would like to have both Frama-C and Why as separated packages.

Here is the situation:

- First with a default why-2.19 installation (a regular ./configure &&
make && make install) Frama-C's configure fails to locate Jc:
checking for no/jc... no
checking for /usr/lib64/ocaml/jessie/jc.cmx... no
configure: WARNING: jc not found

- I figured out this is because why's Makefile doesn't install the JCLIB
and JCCMI_EXPORT files:
#       ??? cp -f $(JCLIB) $(JCCMI_EXPORT) $(LIBDIR)
So I replaced this last line by:
	mkdir -p $(LIBDIR)/ocaml/jessie
 	cp -f $(JCLIB) $(JCCMI_EXPORT) $(LIBDIR)/ocaml/jessie

- Now, Frama-C's configure locates Jc:
checking for no/jc... no
checking for /usr/lib64/ocaml/jessie/jc.cmx... yes

But later the compilation process fails:
Ocamlc       src/jessie/interp.cmi
File "src/jessie/interp.mli", line 26, characters 0-7:
Unbound module Jc
make: *** [src/jessie/interp.cmi] Error 2

So if someone got an idea on how to fix this...

Regards.