Changeset 1634 for src/Clight/test/memorymodel.ma
 Timestamp:
 Jan 4, 2012, 7:42:47 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/test/memorymodel.ma
r961 r1634 29 29 letin r ≝ (store Mint16unsigned store1 Any block 0 (Vint I16 (repr ? 1))); 30 30 31 lapply (refl ? r); elim r in ⊢ (???% → ?) [ whd in ⊢ (??%? → ?)#H destruct31 lapply (refl ? r); elim r in ⊢ (???% → ?); [ whd in ⊢ (??%? → ?); #H destruct 32 32  #rr #_ @rr ] qed. 33 33 … … 36 36 letin r ≝ (store Mint8unsigned store1 Any block 0 (Vint I8 (repr ? 1))); 37 37 38 lapply (refl ? r) elim r in ⊢ (???% → ?) [ whd in ⊢ (??%? → ?)#H destruct38 lapply (refl ? r) elim r in ⊢ (???% → ?); [ whd in ⊢ (??%? → ?); #H destruct 39 39  #rr #_ @ rr ] qed. 40 40 … … 48 48 by the language). *) 49 49 definition store4 := free store3 block. 50 definition store5 : mem. letin r ≝ (free store3 block); whd in r @r qed.50 definition store5 : mem. letin r ≝ (free store3 block); whd in r; @r qed. 51 51 52 52 (* No ordering is imposed on deallocation (even though alloc and free are only used for … … 57 57 definition storeD := free (fst ?? storeCblkC) (snd ?? storeBblkB). 58 58 definition storeE : mem. letin r ≝ (free storeD (snd ?? storeCblkC)). 59 whd in r @r qed.59 whd in r; @r qed. 60 60 61 61 (* Access to the "object representation" (as the C standard puts it) is not specified. *) … … 64 64 definition storeIII : mem. 65 65 letin r ≝ (store Mint32 (fst ?? storeIIblk) Any (snd ?? storeIIblk) 0 (Vint I32 (repr ? 1))); 66 lapply (refl ? r) elim r in ⊢ (???% → ?) [ whd in ⊢ (??%? → ?)#H destruct66 lapply (refl ? r) elim r in ⊢ (???% → ?); [ whd in ⊢ (??%? → ?); #H destruct 67 67  #rr #_ @rr ] qed. 68 68 definition byte := load Mint8unsigned storeIII Any (snd ?? storeIIblk) 0.
Note: See TracChangeset
for help on using the changeset viewer.