Changeset 9 for C-semantics/README


Ignore:
Timestamp:
Jun 21, 2010, 4:22:09 PM (10 years ago)
Author:
campbell
Message:

Enough of an executable semantics to execute a not-quite-trivial program,
plus a patch for compcert to convert C to a matita definition.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • C-semantics/README

    r5 r9  
    1 Status of matita port of CompCert C semantics
    2 =============================================
     1Status of matita port of CompCert 1.6 C semantics
     2=================================================
    33
    4 Last seen working with matita svn r10871.
     4Last seen working with matita svn r10877 with the patch at the bottom of this
     5file.
    56
    67- Most of the memory model has been ported (common/Mem.v -> Mem.ma).
     
    3435  Cexec.ma.  At present only a small subset of expressions and statements
    3536  are handled.
     37
     38* The patch in compcert-1.7.1-matita.patch adds a -dmatita option to
     39  output a matita file containing a definition for the C program.
     40  Note that there must be a "main" function.  (This was made against
     41  1.7.1 for convenience - the Clight syntax is the same as 1.6.)
     42
     43There is a more recent version of compcert available with a revised memory
     44model that may be more closely suited to our needs.
    3645
    3746matita issues and workarounds
     
    119128  haven't been ported yet are done.  The other definitions and most of the
    120129  lemmas still remain to be done.
     130
     131
     132
     133
     134Index: matita/nlibrary/arithmetics/Z.ma
     135===================================================================
     136--- matita/nlibrary/arithmetics/Z.ma    (revision 10877)
     137+++ matita/nlibrary/arithmetics/Z.ma    (working copy)
     138@@ -13,6 +13,7 @@
     139 (**************************************************************************)
     140 
     141 include "arithmetics/nat.ma".
     142+include "arithmetics/compare.ma".
     143 
     144 ninductive Z : Type %G≝%@
     145   OZ : Z
     146@@ -508,7 +509,7 @@
     147    ##[//
     148    ##|#n;nrewrite < (Zsucc_Zplus_pos_O ?);nrewrite > (Zsucc_Zpred ?);//
     149    ##|//]
     150-##|ncases y;//
     151+##|ncases y;/2/
     152 ##|ncases y
     153    ##[#n;nrewrite < (sym_Zplus ??);nrewrite < (sym_Zplus (Zpred OZ) ?);
     154       nrewrite < (Zpred_Zplus_neg_O ?);nrewrite > (Zpred_Zsucc ?);//
Note: See TracChangeset for help on using the changeset viewer.