Changeset 961 for src/Clight/test/memorymodel.ma
- Timestamp:
- Jun 15, 2011, 4:15:52 PM (10 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/Clight/test/memorymodel.ma
r717 r961 27 27 (* write a value *) 28 28 definition store2 : mem. 29 letin r ≝ (store Mint16unsigned store1 Any block 0 (Vint one));29 letin r ≝ (store Mint16unsigned store1 Any block 0 (Vint I16 (repr ? 1))); 30 30 31 31 lapply (refl ? r); elim r in ⊢ (???% → ?) [ whd in ⊢ (??%? → ?) #H destruct … … 34 34 (* overwrite the first byte of the value *) 35 35 definition store3 : mem. 36 letin r ≝ (store Mint8unsigned store1 Any block 0 (Vint one));36 letin r ≝ (store Mint8unsigned store1 Any block 0 (Vint I8 (repr ? 1))); 37 37 38 38 lapply (refl ? r) elim r in ⊢ (???% → ?) [ whd in ⊢ (??%? → ?) #H destruct … … 42 42 example vl_undef: load Mint16signed store3 Any block 0 = Some ? Vundef. @refl qed. 43 43 44 (* The read is successful and returns a signed version ofthe value. *)45 example vl_ok': load Mint8unsigned store3 Any block 0 = Some ? (Vint (zero_ext 8 one)). // qed.44 (* The read is successful and returns the value. *) 45 example vl_ok': load Mint8unsigned store3 Any block 0 = Some ? (Vint I8 (repr ? 1)). // qed. 46 46 47 47 (* NB: Double frees are allowed by the memory model (although not necessarily … … 63 63 definition storeIIblk := alloc storeA 0 4 Any. 64 64 definition storeIII : mem. 65 letin r ≝ (store Mint32 (fst ?? storeIIblk) Any (snd ?? storeIIblk) 0 (Vint one));65 letin r ≝ (store Mint32 (fst ?? storeIIblk) Any (snd ?? storeIIblk) 0 (Vint I32 (repr ? 1))); 66 66 lapply (refl ? r) elim r in ⊢ (???% → ?) [ whd in ⊢ (??%? → ?) #H destruct 67 67 | #rr #_ @rr ] qed.
Note: See TracChangeset
for help on using the changeset viewer.