Project

General

Profile

Actions
Copy link

Bug #1450

closed

Compatibility with Ocaml 3.12

Added by Alexey Khoroshilov over 13 years ago. Updated over 13 years ago.

Status:
Closed
Priority:
High
Assignee:
Pavel Shved
Category:
-
Target version:
2.6
Start date:
06/28/2011
Due date:
07/06/2011
% Done:

0%

Estimated time:
Detected in build:
svn
Platform:
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

Actions
Copy link
 #1

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.

Actions
Copy link
 #2

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.

Actions
Copy link
 #3

Updated by Pavel Shved over 13 years ago

  • Status changed from New to Resolved
Actions
Copy link
 #4

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'

Actions
Copy link
 #5

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?

Actions
Copy link
 #6

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'

Actions
Copy link
 #7

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)?

Actions
Copy link
 #8

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.

Actions
Copy link
 #9

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.

Actions
Copy link
 #10

Updated by Alexey Khoroshilov over 13 years ago

  • Status changed from Resolved to Closed
Actions
Copy link
 #11

Updated by Pavel Shved over 13 years ago

  • Project changed from Linux Driver Verification to BLAST
  • Category deleted (BLAST)
Actions
Copy link
 #12

Updated by Pavel Shved over 13 years ago

  • Target version set to 2.6
Actions
Copy link

Also available in: Atom PDF