ocaml-3.08.3 for blast model checker

ocaml-3.08.3 for blast model checker

[Suzanne Wood]

[-- Warning: decoded text below may be mangled, UTF-8 assumed --]
[-- Attachment #1: Type: text/plain, Size: 1265 bytes --]

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
3.08.04.
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.

Re: [Caml-list] ocaml-3.08.3 for blast model checker

[Xavier Leroy]

[-- Attachment #1: Type: text/plain, Size: 224 bytes --]

> But, in trying to compile ocaml-3.08.3, "make world" dies with:
> [...]

You could take otherlibs/num/bng_ia32.c from the 3.08.4 distribution.
Equivalently, apply the attached patch to your 3.08.3 sources.

- Xavier Leroy

[-- Attachment #2: patch --]
[-- Type: text/plain, Size: 1958 bytes --]

Index: bng_ia32.c
===================================================================
RCS file: /net/yquem/devel/caml/repository/csl/otherlibs/num/bng_ia32.c,v
retrieving revision 1.3.6.1
retrieving revision 1.3
diff -c -r1.3.6.1 -r1.3
*** bng_ia32.c	20 Jul 2005 08:18:59 -0000	1.3.6.1
--- bng_ia32.c	26 Oct 2003 09:51:11 -0000	1.3
***************
*** 11,17 ****
  /*                                                                     */
  /***********************************************************************/
  
! /* $Id: bng_ia32.c,v 1.3.6.1 2005/07/20 08:18:59 xleroy Exp $ */
  
  /* Code specific to the Intel IA32 (x86) architecture. */
  
--- 11,17 ----
  /*                                                                     */
  /***********************************************************************/
  
! /* $Id: bng_ia32.c,v 1.3 2003/10/26 09:51:11 xleroy Exp $ */
  
  /* Code specific to the Intel IA32 (x86) architecture. */
  
***************
*** 121,128 ****
          "leal 4(%1), %1 \n\t"
          "decl %2 \n\t"
          "jnz 1b"
!         : "+&r" (a), "+&r" (b), "+&r" (blen), "=m" (out)
!         : "m" (d)
          : "eax", "edx");
    }
    if (alen == 0) return out;
--- 121,128 ----
          "leal 4(%1), %1 \n\t"
          "decl %2 \n\t"
          "jnz 1b"
!         : "+&r" (a), "+&r" (b), "+&rm" (blen), "+&r" (out)
!         : "rm" (d)
          : "eax", "edx");
    }
    if (alen == 0) return out;
***************
*** 164,171 ****
          "leal 4(%1), %1 \n\t"
          "decl %2 \n\t"
          "jnz 1b"
!         : "+&r" (a), "+&r" (b), "=m" (blen), "=m" (out), "=&r" (tmp)
!         : "m" (d)
          : "eax", "edx");
    }
    if (alen == 0) return out;
--- 164,171 ----
          "leal 4(%1), %1 \n\t"
          "decl %2 \n\t"
          "jnz 1b"
!         : "+&r" (a), "+&r" (b), "+&rm" (blen), "+&rm" (out), "=&r" (tmp)
!         : "rm" (d)
          : "eax", "edx");
    }
    if (alen == 0) return out;