Changeset 1634


Ignore:
Timestamp:
Jan 4, 2012, 7:42:47 PM (8 years ago)
Author:
campbell
Message:

Update memory model examples syntax.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/test/memorymodel.ma

    r961 r1634  
    2929  letin r ≝ (store Mint16unsigned store1 Any block 0 (Vint I16 (repr ? 1)));
    3030
    31   lapply (refl ? r); elim r in ⊢ (???% → ?) [ whd in ⊢ (??%? → ?) #H destruct
     31  lapply (refl ? r); elim r in ⊢ (???% → ?); [ whd in ⊢ (??%? → ?); #H destruct
    3232  | #rr #_ @rr ] qed.
    3333
     
    3636  letin r ≝ (store Mint8unsigned store1 Any block 0 (Vint I8 (repr ? 1)));
    3737
    38   lapply (refl ? r) elim r in ⊢ (???% → ?) [ whd in ⊢ (??%? → ?) #H destruct
     38  lapply (refl ? r) elim r in ⊢ (???% → ?); [ whd in ⊢ (??%? → ?); #H destruct
    3939  | #rr #_ @ rr ] qed.
    4040 
     
    4848       by the language). *)
    4949definition store4 := free store3 block.
    50 definition store5 : mem. letin r ≝ (free store3 block); whd in r @r qed.
     50definition store5 : mem. letin r ≝ (free store3 block); whd in r; @r qed.
    5151
    5252(* No ordering is imposed on deallocation (even though alloc and free are only used for
     
    5757definition storeD := free (fst ?? storeCblkC) (snd ?? storeBblkB).
    5858definition storeE : mem. letin r ≝ (free storeD (snd ?? storeCblkC)).
    59 whd in r @r qed.
     59whd in r; @r qed.
    6060
    6161(* Access to the "object representation" (as the C standard puts it) is not specified. *)
     
    6464definition storeIII : mem.
    6565 letin r ≝ (store Mint32 (fst ?? storeIIblk) Any (snd ?? storeIIblk) 0 (Vint I32 (repr ? 1)));
    66   lapply (refl ? r) elim r in ⊢ (???% → ?) [ whd in ⊢ (??%? → ?) #H destruct
     66  lapply (refl ? r) elim r in ⊢ (???% → ?); [ whd in ⊢ (??%? → ?); #H destruct
    6767  | #rr #_ @rr ] qed.
    6868definition byte := load Mint8unsigned storeIII Any (snd ?? storeIIblk) 0.
Note: See TracChangeset for help on using the changeset viewer.