Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[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

  • Subject: [Frama-c-discuss] How to compil Frama-C with an existing Why installation
  • From: jcdemay at rennes.supelec.fr (Jonathan-Christofer Demay)
  • Date: Tue, 14 Jul 2009 05:02:00 +0200
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.