Changeset 409 for Deliverables/D3.1/C-semantics/test/memorymodel.ma
- Timestamp:
- Dec 13, 2010, 3:58:29 PM (10 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
Deliverables/D3.1/C-semantics/test/memorymodel.ma
r12 r409 21 21 store. *) 22 22 ndefinition store0 := empty. 23 ndefinition store1block : mem × block ≝ alloc store0 0 4 .23 ndefinition store1block : mem × block ≝ alloc store0 0 4 Any. 24 24 ndefinition store1 : mem ≝ fst ?? store1block. 25 25 ndefinition block := snd ?? store1block. … … 27 27 (* write a value *) 28 28 ndefinition store2 : mem. 29 nletin r ≝ (store Mint16unsigned store1 block 0 (Vint one));29 nletin r ≝ (store Mint16unsigned store1 Any block 0 (Vint one)); 30 30 31 31 nlapply (refl ? r); nelim r in ⊢ (???% → ?);##[ nwhd in ⊢ (??%? → ?); #H; ndestruct; … … 34 34 (* overwrite the first byte of the value *) 35 35 ndefinition store3 : mem. 36 nletin r ≝ (store Mint8unsigned store1 block 0 (Vint one));36 nletin r ≝ (store Mint8unsigned store1 Any block 0 (Vint one)); 37 37 38 38 nlapply (refl ? r); nelim r in ⊢ (???% → ?);##[ nwhd in ⊢ (??%? → ?); #H; ndestruct; … … 40 40 41 41 (* The size checking rejects the read and gives us Some Vundef. *) 42 nremark vl_undef: load Mint16signed store3 block 0 = Some ? Vundef. //; nqed.42 nremark vl_undef: load Mint16signed store3 Any block 0 = Some ? Vundef. //; nqed. 43 43 44 44 (* The read is successful and returns a signed version of the value. *) 45 nremark vl_ok': load Mint8unsigned store3 block 0 = Some ? (Vint (zero_ext 8 one)). //; nqed.45 nremark vl_ok': load Mint8unsigned store3 Any block 0 = Some ? (Vint (zero_ext 8 one)). //; nqed. 46 46 47 47 (* NB: Double frees are allowed by the memory model (although not necessarily … … 53 53 stack memory in the semantics. *) 54 54 ndefinition storeA := empty. 55 ndefinition storeBblkB := alloc storeA 0 4 .56 ndefinition storeCblkC := alloc (fst ?? storeBblkB) 0 8 .55 ndefinition storeBblkB := alloc storeA 0 4 Any. 56 ndefinition storeCblkC := alloc (fst ?? storeBblkB) 0 8 Any. 57 57 ndefinition storeD := free (fst ?? storeCblkC) (snd ?? storeBblkB). 58 58 ndefinition storeE : mem. nletin r ≝ (free storeD (snd ?? storeCblkC)). … … 61 61 (* Access to the "object representation" (as the C standard puts it) is not specified. *) 62 62 ndefinition storeI := empty. 63 ndefinition storeIIblk := alloc storeA 0 4 .63 ndefinition storeIIblk := alloc storeA 0 4 Any. 64 64 ndefinition storeIII : mem. 65 nletin r ≝ (store Mint32 (fst ?? storeIIblk) (snd ?? storeIIblk) 0 (Vint one));65 nletin r ≝ (store Mint32 (fst ?? storeIIblk) Any (snd ?? storeIIblk) 0 (Vint one)); 66 66 nlapply (refl ? r); nelim r in ⊢ (???% → ?);##[ nwhd in ⊢ (??%? → ?); #H; ndestruct; 67 67 ##| #rr; #_; napply rr ##] nqed. 68 ndefinition byte := load Mint8unsigned storeIII (snd ?? storeIIblk) 0.68 ndefinition byte := load Mint8unsigned storeIII Any (snd ?? storeIIblk) 0. 69 69 nremark byteundef: byte = Some ? Vundef. //; nqed. (* :( *)
Note: See TracChangeset
for help on using the changeset viewer.