English version
Accueil     À propos     Téléchargement     Ressources     Contactez-nous    

Ce site est rarement mis à jour. Pour les informations les plus récentes, rendez-vous sur le nouveau site OCaml à l'adresse ocaml.org.

Browse thread
ocaml-3.08.3 for blast model checker
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: 2005-12-02 (00:34)
From: Suzanne Wood <suzannew@c...>
Subject: ocaml-3.08.3 for blast model checker
Having had no problem installing ocaml-3.09.0, it looks like I need
to install ocaml-3.08.3 for use with the UC Berkeley Blast software
model checker, per the following advisory:
"Release note: We have to distribute one part of Blast precompiled
(the foci library, which implements the craig interpolation),
because the code is copyrighted by Cadence labs, Berkeley.
Unfortunately, this precompiled piece is not compatible with OCaml
A working example configuration for compiling Blast 2.0 is
OCaml 3.08.3 and gcc (GCC) 3.4.4 20050721 (Red Hat 3.4.4-2).
--Dirk 2005-10-18"

But, in trying to compile ocaml-3.08.3, "make world" dies with:
make[1]: Leaving directory ` /ocaml-3.08.3/otherlibs/str'
make[1]: Entering directory ` /ocaml-3.08.3/otherlibs/num'
gcc -O -I../../byterun -fno-defer-pop -Wall -D_FILE_OFFSET_BITS=64
-D_REENTRANT -fPIC -DBNG_ARCH_ia32 -DBNG_ASM_LEVEL=2   -c -o bng.o bng.c
In file included from bng.c:21:
bng_ia32.c: In function ‘bng_ia32_mult_sub_digit’:
bng_ia32.c:153: error: can't find a register in class ‘GENERAL_REGS’
while reloading ‘asm’
make[1]: *** [bng.o] Error 1
make[1]: Leaving directory ` /ocaml-3.08.3/otherlibs/num'
make: *** [otherlibraries] Error 2

Thank you for any suggestion about how to proceed.