From 28c04de64220be15c589c4dbe1662b212b6d25b1 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 4 Sep 2010 10:14:37 +0000 Subject: Updated git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1505 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- README | 21 ++++++++++++++++++--- 1 file changed, 18 insertions(+), 3 deletions(-) (limited to 'README') diff --git a/README b/README index 44a845e..29cd47f 100644 --- a/README +++ b/README @@ -39,6 +39,9 @@ SUPPORTED PLATFORMS: - ARM / Linux [experimental] For ARM machines running the Linux operating system. +- IA32 / Linux, BSD, MacOS [experimental] + For Intel/AMD x86 processors with SSE2 extensions + (i.e. Pentium 4 and later). PREREQUISITES: @@ -46,7 +49,7 @@ PREREQUISITES: the search path. For MacOS X, you can get them by installing the XCode development tools, as found on the installation DVDs. -* The Coq proof assistant, version 8.2-1 or later. +* The Coq proof assistant, version 8.2pl1 or 8.2pl2. Coq is free software, available from http://coq.inria.fr/ * The Caml functional language, version 3.10 or later. @@ -64,6 +67,9 @@ where is one of: ppc-macosx (PowerPC, MacOS X) ppc-linux (PowerPC, Linux) arm-linux (ARM, Linux) + ia32-linux (x86 SSE2 32 bits, Linux) + ia32-bsd (x86 SSE2 32 bits, BSD) + ia32-macosx (x86 SSE2 32 bits, MacOS X) This generates the Makefile.config file in the top directory. @@ -74,6 +80,7 @@ The "configure" script accepts the following options: -libdir (default: /usr/local/lib/compcert) Directory where the Compcert support library will be installed + (needed only under MacOS X) -prefix (default: /usr/local) Set bindir and libdir to @@ -143,7 +150,7 @@ Preprocessing options: -U Undefine preprocessor symbol Language support options (use -fno- to turn off -f) : -fbitfields Emulate bit fields in structs [off] - -flonglong Treat 'long long' as 'long' and 'long double' as 'double' [off] + -flonglong Partial emulation of 'long long' types [on] -fstruct-passing Emulate passing structs and unions by value [off] -fstruct-assign Emulate assignment between structs or unions [off] -fvararg-calls Emulate calls to variable-argument functions [on] @@ -153,14 +160,22 @@ Code generation options: -fsmall-const Set maximal size for allocation in small constant area Tracing options: -dparse Save C file after parsing and elaboration in .parse.c + -dc Save generated Compcert C in .compcert.c -dclight Save generated Clight in .light.c + -dcminor Save generated Cminor in .cm + -drtl Save unoptimized generated RTL in .rtl + -dtailcall Save RTL after tail call optimization in .tailcall.rtl + -dcastopt Save RTL after cast optimization in .castopt.rtl + -dconstprop Save RTL after constant propagation in .constprop.rtl + -dcse Save RTL after CSE optimization in .cse.rtl + -dalloc Save LTL after register allocation in .alloc.ltl -dasm Save generated assembly in .s Linking options: -l Link library -L Add to search path for libraries -o Generate executable in (default: a.out) General options: - -stdlib Set the path of the Compcert run-time library + -stdlib Set the path of the Compcert stdlib wrappers -v Print external commands before invoking them -- cgit v1.2.3