Merge of the reuse-temps branch:

- Reload temporaries are marked as destroyed (set to Vundef) across
  operations in the semantics of LTL, LTLin, Linear and Mach, 
  allowing Asmgen to reuse them.
- Added IA32 port.
- Cleaned up float conversions and axiomatization of floats.



git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1499 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 30 insertions, 0 deletions

diff --git a/configure b/configure
index f72e981..d061396 100755
--- a/configure
+++ b/configure
@@ -33,6 +33,9 @@ Supported targets:
   ppc-macosx       (PowerPC, MacOS X)
   ppc-linux        (PowerPC, Linux)
   arm-linux        (ARM, Linux)
+  ia32-linux       (x86 32 bits, Linux)
+  ia32-bsd         (x86 32 bits, BSD)
+  ia32-macosx      (x86 32 bits, MacOS X)
   manual           (edit configuration file by hand)
 
 Options:
@@ -89,6 +92,33 @@ case "$target" in
     casm="gcc -c"
     clinker="gcc"
     libmath="-lm";;
+  ia32-linux)
+    arch="ia32"
+    variant="standard"
+    system="linux"
+    cc="gcc -m32"
+    cprepro="gcc -m32 -U__GNUC__ -E"
+    casm="gcc -m32 -c"
+    clinker="gcc -m32"
+    libmath="-lm";;
+  ia32-bsd)
+    arch="ia32"
+    variant="standard"
+    system="bsd"
+    cc="gcc -m32"
+    cprepro="gcc -m32 -U__GNUC__ -E"
+    casm="gcc -m32 -c"
+    clinker="gcc -m32"
+    libmath="-lm";;
+  ia32-macosx)
+    arch="ia32"
+    variant="standard"
+    system="macosx"
+    cc="gcc -arch i386"
+    cprepro="gcc -arch i386 -U__GNUC__ -U__BLOCKS__ -E"
+    casm="gcc -arch i386 -c"
+    clinker="gcc -arch i386"
+    libmath="";;
   manual)
     ;;
   "")