Changeset 178


Ignore:
Timestamp:
Oct 13, 2010, 12:19:30 PM (9 years ago)
Author:
campbell
Message:

Bring README file up to date.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • C-semantics/README

    r15 r178  
    22=================================================
    33
    4 Last seen working with matita svn r10890.
     4Last seen working with matita svn r10960 with 10957 reverted.
    55
    66- Most of the memory model has been ported (common/Mem.v -> Mem.ma).
     
    1616  the semantics.
    1717
    18 - Most of the small-step C semantics has been ported, although much of the
    19   underlying arithmetic and environment functions are only present as axioms,
    20   including the type of identifiers.
     18- Most of the small-step C semantics has been ported, although a few of the
     19  underlying arithmetic functions are only present as axioms.
    2120
    22 - Nonetheless, this is sufficient to show the semantics of a trivial C program
    23   in test/trivial.ma.
     21- Nonetheless, this is sufficient to animate the semantics of several simple C
     22  programs in test.
    2423
    2524- A collection of definitions and lemmas that probably ought to be in
     
    3130  as a functor on the word size - we don't have an equivalent of this yet.
    3231
    33 * Some experimental work on an executable semantics has been started in
    34   Cexec.ma.  At present only a small subset of expressions and statements
    35   are handled.
     32* The executable semantics can be found in CexecIO.ma, which uses the
     33  resumption monad defined in IOMonad.ma.
     34
     35* The patch in acc-0.1.spaces.patch adds a -ma option to the prototype
     36  compiler which outputs a matita file containing the Clight program as
     37  a definition usable by the semantics.  It also adds parsing support for
     38  the memory space extensions (__data and friends).
    3639
    3740* The patch in compcert-1.7.1-matita.patch adds a -dmatita option to
     
    3942  Note that there must be a "main" function.  (This was made against
    4043  1.7.1 for convenience - the Clight syntax is the same as 1.6.)
     44  This is an older version of the prototype compiler patch, and lacks the
     45  memory extensions.
    4146
    4247There is a more recent version of compcert available with a revised memory
     
    7883AST.ma
    7984
    80   Program transformation sections left alone.
     85  Program transformation sections mostly left alone.
    8186
    8287Coqlib.ma
     
    108113Floats.ma
    109114
    110   Axiomatised, but so was the original!
     115  Axiomatised, but so was the original!  Likely to be removed because we do
     116  not intend to support floating point.
    111117
    112118Globalenvs.ma
    113119
    114   Basic definition only.
     120  Basic definition only; sufficient for animating the semantics.
    115121
    116122Integers.ma
     
    132138
    133139  Ported definitions for multiple steps and program behaviour; left
    134   alternative definitions, some lemmas, plus simulations sections for later.
     140  alternative definitions, some lemmas, plus most of the simulations sections
     141  for later.
    135142
    136143Values.ma
Note: See TracChangeset for help on using the changeset viewer.