Bug #1450
closed
Compatibility with Ocaml 3.12
Added by Alexey Khoroshilov over 13 years ago.
Updated about 13 years ago.
Published in build:
eb82645
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
- Due date set to 07/06/2011
CIL has an upstream? O_o
Ok, will fix soon.
- 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.
- Status changed from New to Resolved
- 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'
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?
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'
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)?
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.
- Status changed from Open to Resolved
Applied the fix in commit:c69d66b9, tested on Alexey's new machine.
- Status changed from Resolved to Closed
- Project changed from Linux Driver Verification to BLAST
- Category deleted (
BLAST)
- Target version set to 2.6
Also available in: Atom
PDF