Changeset 12 for C-semantics/test


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

Make memory model tests more readable.
Update README.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • 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.