Version française
Home     About     Download     Resources     Contact us    

This site is updated infrequently. For up-to-date information, please visit the new OCaml website at

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.