Changeset 12


Ignore:
Timestamp:
Jul 7, 2010, 6:46:46 PM (10 years ago)
Author:
campbell
Message:

Make memory model tests more readable.
Update README.

Location:
C-semantics
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • C-semantics/README

    r9 r12  
    22=================================================
    33
    4 Last seen working with matita svn r10877 with the patch at the bottom of this
    5 file.
     4Last seen working with matita svn r10890.
    65
    76- Most of the memory model has been ported (common/Mem.v -> Mem.ma).
     
    2827
    2928- Some of the machine integers (i.e., integers modulo) results are
    30   given as axioms in Integers.ma.  Implementing them could be
    31   difficult if we keep using a unary representation of integers as
    32   formalisation involves constants like 2^32.
     29  given as axioms in Integers.ma.  Implementing them should be routine now that
     30  we have a binary representation of integers.  The CompCert version is given
     31  as a functor on the word size - we don't have an equivalent of this yet.
    3332
    3433* Some experimental work on an executable semantics has been started in
     
    6766AST.ma
    6867
    69   No concrete type for ident.
    7068  Program transformation sections left alone.
    7169
     
    7371
    7472  Only essential parts:
    75   - "align" is axiomatised
     73  - align
     74  - some 2^n lemmas (which could go into the binary libraries)
    7675  - option_map
    7776  - parts of list disjointness and non-repetition
     
    116115Mem.ma
    117116
    118   Everything except for omega in proofs.
     117  Everything except for omega in proofs.  Much of the transformations sections
     118  are commented out until Integers.ma is done properly.
    119119
    120120Smallstep.ma
     
    130130
    131131
    132 
    133 
    134 Index: 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 ?);//
  • C-semantics/test/memorymodel.ma

    r3 r12  
    2424ndefinition store1 : mem ≝ fst ?? store1block.
    2525ndefinition block := snd ?? store1block.
     26
    2627(* write a value *)
    2728ndefinition store2 : mem.
    2829  nletin r ≝ (store Mint16unsigned store1 block 0 (Vint one));
     30
    2931  nlapply (refl ? r); nelim r in ⊢ (???% → ?);##[ nwhd in ⊢ (??%? → ?); #H; ndestruct;
    3032  ##| #rr; #_; napply rr ##] nqed.
     33
    3134(* overwrite the first byte of the value *)
    3235ndefinition store3 : mem.
    3336  nletin r ≝ (store Mint8unsigned store1 block 0 (Vint one));
     37
    3438  nlapply (refl ? r); nelim r in ⊢ (???% → ?);##[ nwhd in ⊢ (??%? → ?); #H; ndestruct;
    3539  ##| #rr; #_; napply rr ##] nqed.
    3640 
    37 ndefinition vl := load Mint16signed store3 block 0.
    3841(* The size checking rejects the read and gives us Some Vundef. *)
    39 nremark vl_undef: vl = Some ? Vundef. //; nqed.
     42nremark vl_undef: load Mint16signed store3 block 0 = Some ? Vundef. //; nqed.
    4043
    41 ndefinition vl' := load Mint8unsigned store3 block 0.
    4244(* The read is successful and returns a signed version of the value. *)
    43 nremark vl_ok': vl' = Some ? (Vint (zero_ext 8 one)). //; nqed.
     45nremark vl_ok': load Mint8unsigned store3 block 0 = Some ? (Vint (zero_ext 8 one)). //; nqed.
    4446
    45 ndefinition store4 := free store3 block.
    4647(* NB: Double frees are allowed by the memory model (although not necessarily
    4748       by the language). *)
     49ndefinition store4 := free store3 block.
    4850ndefinition store5 : mem. nletin r ≝ (free store3 block); nwhd in r; napply r; nqed.
    4951
Note: See TracChangeset for help on using the changeset viewer.