From 6f731da1e13d295104d624114ee26db46e50238f Mon Sep 17 00:00:00 2001 From: xleroy Date: Tue, 30 Mar 2010 15:31:24 +0000 Subject: Updates for release 1.7 git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1305 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- Changelog | 46 ++++++++++++++++++++++++++++++++++++++++++++++ README | 27 ++++++++++++++++++--------- 2 files changed, 64 insertions(+), 9 deletions(-) diff --git a/Changelog b/Changelog index 750048da..45dd53d9 100644 --- a/Changelog +++ b/Changelog @@ -1,3 +1,49 @@ +Release 1.7, 2010-03-31 +======================= + +- New implementation of the C type-checker, simplifier, and translation to + Clight. Compared with the previous CIL-based solution, the new + implementation is more modular and supports more optional simplifications. + +- More features of the C language are handled by expansion during + translation to Clight: + . assignment between structs and unions (option -fstruct-assign) + . passing structs and union by value (option -fstruct-passing) + . bit-fields in structs (option -fbitfields) + +- The "volatile" modifier is now honored. Volatile accesses are represented + in Clight by calls to built-in functions, which are preserved throughout + the compilation chain, then turned into processor loads and stores + at the end. + +- Generic support for C built-in functions. These predefined external + functions give access to special instructions of the processor. See + powerpc/CBuiltins.ml for the list of PowerPC built-in functions. + +- The memory model now exposes the bit-level in-memory representation + of integers and floats. This strengthens the semantic preservation + theorem: we now prove that C code that directly manipulates these + bit-level representations (e.g. via a union between floats and integers) + is correctly compiled. + +- The memory model now supports fine-grained access control to individual + bytes of a memory block. This feature is currently unused in the + compiler proofs, but will facilitate connections with separation logics + later. + +- External functions are now allowed to read and modify memory. + The semantic preservation proofs were strengthened accordingly. + In particular, this enables the malloc() and free() C library functions + to be modeled as external functions in a provably correct manner. + +- Minor improvements in the handling of global environments and the + construction of the initial memory state. + +- Bug fixes in the handling of '#pragma section' and '#pragma set_section'. + +- The C test suite was enriched and restructured. + + Release 1.6, 2010-01-13 ======================= diff --git a/README b/README index 42f0443c..44a845e8 100644 --- a/README +++ b/README @@ -19,7 +19,7 @@ purposes. COPYRIGHT: The Compcert verified compiler is Copyright 2004, 2005, 2006, 2007, -2008, 2009 Institut National de Recherche en Informatique et en +2008, 2009, 2010 Institut National de Recherche en Informatique et en Automatique (INRIA). It is distributed under the conditions stated in file LICENSE. @@ -27,7 +27,7 @@ file LICENSE. SUPPORTED PLATFORMS: - PowerPC / MacOS [stable] - For Apple Macs running the MacOS 10.4 or 10.5 operating system. + For Apple Macs running the MacOS 10.4, 10.5 or 10.6 operating system. Both PowerPC-based and Intel-based Macs are supported. The PowerPC code generated by the Compcert compiler runs natively at full speed on PowerPC-based Macs, and runs under @@ -65,8 +65,7 @@ where is one of: ppc-linux (PowerPC, Linux) arm-linux (ARM, Linux) -This generates the Makefile.config file in the top directory -and prepares and configures the CIL library in the cil/ subdirectory. +This generates the Makefile.config file in the top directory. The "configure" script accepts the following options: @@ -85,9 +84,9 @@ The "configure" script accepts the following options: make all This re-checks all the Coq proofs, then extracts Caml code from the -Coq specification and combines it with the CIL library and supporting -hand-written Caml code to generate the executable for Compcert. This -step takes 10 to 15 minutes on a recent Mac computer; be patient. +Coq specification and combines it with supporting hand-written Caml +code to generate the executable for Compcert. This step takes 10 to +15 minutes on a recent Mac computer; be patient. 3- You can now install Compcert. This will create the "ccomp" command in the binary directory selected during configuration, and install @@ -142,8 +141,18 @@ Preprocessing options: -I Add to search path for #include files -D= Define preprocessor symbol -U Undefine preprocessor symbol -Compilation options: - -flonglong Treat 'long long' as 'long' and 'long double' as 'double' +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] + -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] +Code generation options: + -fmadd Use fused multiply-add and multiply-sub instructions + -fsmall-data Set maximal size for allocation in small data area + -fsmall-const Set maximal size for allocation in small constant area +Tracing options: + -dparse Save C file after parsing and elaboration in .parse.c -dclight Save generated Clight in .light.c -dasm Save generated assembly in .s Linking options: -- cgit