Bug #1450
closedCompatibility with Ocaml 3.12
0%
Description
Our tools cannot be built with ocaml 3.12.
The main issue is absence of a library linked with '-lstr' option.
Starting from ocaml-3.12.0 -lcamlstr should be used instead of -lstr.
For cil there is an upstream patch:
cilly: $(OBJDIR)/cilly$(EXE)
$(OBJDIR)/cilly$(EXE) : $(CILLY_MODULES:%=$(OBJDIR)/%.$(CMO)) \
$(CILLY_CMODULES:%=$(OBJDIR)/%.$(CMC))
@$(NARRATIVE) "Linking $(COMPILETOWHAT) $@ $(LINKMSG)"
$(AT)$(CAMLLINK) -verbose -o $@ \
$(CILLY_LIBS:%=%.$(CMXA)) \
- $(CILLY_LIBS:%=-cclib -l%) \
$^
For blast may be useful Debian patch:
--- a/configure
+++ b/configure
@@ -680,6 +680,15 @@ if [ $enable_apache -gt 0 ]; then
exit 1
fi
+ case `ocamlc -version` in
+ 3.12*)
+ str_stubs=-lcamlstr
+ ;;
+ *)
+ str_stubs=-lstr
+ ;;
+ esac
+
fi
-APACHE_OCAMLLIBS = -lcamlrun -ltermcap -lunix -lstr
+APACHE_OCAMLLIBS = -lcamlrun -ltermcap -lunix $str_stubs
Updated by Pavel Shved over 13 years ago
- Due date set to 07/06/2011
CIL has an upstream? O_o
Ok, will fix soon.
Updated by Pavel Shved over 13 years ago
- Published in build set to eb82645
CIL upstream commit has been cherry-picked.
As for OCaml issue, I prefer another solution. Instead of hardcoding version numbers, which will eventually change and bring other bugs, I wrote a small "configure" shell script to check for availability of "OCaml libraries"—whatever they actually are:
ocamlopt.opt empty.ml -cclib '-lstr' >/dev/null 2>/dev/null echo $$?
(where empty.ml is an empty file). This will print 0 if -lstr is available; if it's not, then we link against -lcamlstr.
The fixes are available in commit:eb82645.
Updated by Alexey Khoroshilov over 13 years ago
- Status changed from Resolved to Open
It looks like it does not work:
Linking OCAML (byte code) program pblast.byte ocamlc.opt -I /home/tester/ldv/ldv-tools/dscv/rcv/backends/blast/blast/lib -o pblast.byte -custom nums.cma str.cma unix.cma libutils.cma libcaddie.cma libcil.cma ./obj/ast.cmo ./obj/blastArch.cmo ./obj/lvalUtils.cmo ./obj/constraintUtil.cmo ./obj/inputparse.cmo ./obj/inputflex.cmo ./obj/SMTLIBInterface.cmo ./obj/fociInterface.cmo ./obj/csisatInterface.cmo ./obj/theoremProver.cmo ./obj/blastControlFlowAutomaton.cmo ./obj/blastCilInterface.cmo ./obj/blastCSystemDescr.cmo ./obj/bddptsto.cmo ./obj/aliasAnalyzer.cmo ./obj/predBdd.cmo ./obj/predTable.cmo ./obj/absutil.cmo ./obj/events.cmo ./obj/symbolicStore.cmo ./obj/eventCounterLattice.cmo ./obj/listLatticeUtil.cmo ./obj/lattice.cmo ./obj/listLattice.cmo ./obj/unionlattice.cmo ./obj/sourceStats.cmo ./obj/abstraction.cmo ./obj/cfAbstraction.cmo ./obj/modelChecker.cmo ./obj/lazyModelChecker.cmo ./obj/cfLazyModelChecker.cmo ./obj/cfbLazyModelChecker.cmo ./obj/main.cmo \ -cc g++ -cclib '-L /home/tester/ldv/ldv-tools/dscv/rcv/backends/blast/blast/lib -lnums -lstr -lunix -lcaddie-c-part -ldddmp -lcudd -lepd -lutil -lst -lmtr -lperfcount -lstdc++' /usr/bin/ld: cannot find -lstr collect2: ld returned 1 exit status File "_none_", line 1, characters 0-1: Error: Error while building custom runtime system make[5]: *** [pblast.byte] Error 2 make[5]: Leaving directory `/home/tester/ldv/ldv-tools/dscv/rcv/backends/blast/blast/psrc'
Updated by Pavel Shved over 13 years ago
Yeah, I felt that sometning will go wrong... The command a couple of posts above is correct; I just changed it to a one with -c (without testing, sorry for that), so that it would skip the linking stage--which was necessary to check if the library is there in the first place.
Could you please fix that for me?
Updated by Alexey Khoroshilov over 13 years ago
I have fixed that locally and blast has been built, but the next issue appears:
make -C cil make[3]: Entering directory `/home/tester/ldv/ldv-tools/dscv/rcv/cil' Linking bytecode obj/x86_LINUX/cilly.byte.exe + gcc -o 'obj/x86_LINUX/cilly.byte.exe' '-L/usr/lib64/ocaml' -g '/tmp/camlprimf32a45.c' '-lcamlstr' '-lunix' '-lunix' '-lstr' 'obj/x86_LINUX/perfcount.o' '-lcamlrun' -I'/usr/lib64/ocaml' -lm -ldl -lcurses -lpthread /usr/bin/ld: cannot find -lstr collect2: ld returned 1 exit status File "_none_", line 1, characters 0-1: Error: Error while building custom runtime system make[3]: *** [obj/x86_LINUX/cilly.byte.exe] Error 2 make[3]: Leaving directory `/home/tester/ldv/ldv-tools/dscv/rcv/cil' make[2]: *** [cil] Error 2 make[2]: Leaving directory `/home/tester/ldv/ldv-tools/dscv/rcv'
Updated by Pavel Shved over 13 years ago
Oh, it's CIL inside DSCV failing (I only tested CIL inside BLAST).
Could you, please, pull master in its folder as well (ldv-tools/dscv/rcv/cil)?
Updated by Evgeny Novikov over 13 years ago
From today Alexey is on his holiday for a couple of weeks. So, I'll be able to apply your request on the next week after Wednesday.
Updated by Pavel Shved over 13 years ago
- Status changed from Open to Resolved
Applied the fix in commit:c69d66b9, tested on Alexey's new machine.
Updated by Alexey Khoroshilov over 13 years ago
- Status changed from Resolved to Closed
Updated by Pavel Shved about 13 years ago
- Project changed from Linux Driver Verification to BLAST
- Category deleted (
BLAST)