Changeset 409 for Deliverables/D3.1/C-semantics/test/memorymodel.ma

Timestamp:

Dec 13, 2010, 3:58:29 PM (9 years ago)

Author:

campbell

Message:

Update a couple of examples; put support for animation in its own file.

File:

• Deliverables/D3.1/C-semantics/test/memorymodel.ma (modified) (6 diffs)

Deliverables/D3.1/C-semantics/test/memorymodel.ma

@@ -21 +21 @@
    store. *)
 ndefinition store0 := empty.
-ndefinition store1block : mem × block ≝ alloc store0 0 4.
+ndefinition store1block : mem × block ≝ alloc store0 0 4 Any.
 ndefinition store1 : mem ≝ fst ?? store1block.
 ndefinition block := snd ?? store1block.
@@ -27 +27 @@
 (* write a value *)
 ndefinition store2 : mem.
-  nletin r ≝ (store Mint16unsigned store1 block 0 (Vint one));
+  nletin r ≝ (store Mint16unsigned store1 Any block 0 (Vint one));
 
   nlapply (refl ? r); nelim r in ⊢ (???% → ?);##[ nwhd in ⊢ (??%? → ?); #H; ndestruct;
@@ -34 +34 @@
 (* overwrite the first byte of the value *)
 ndefinition store3 : mem.
-  nletin r ≝ (store Mint8unsigned store1 block 0 (Vint one));
+  nletin r ≝ (store Mint8unsigned store1 Any block 0 (Vint one));
 
   nlapply (refl ? r); nelim r in ⊢ (???% → ?);##[ nwhd in ⊢ (??%? → ?); #H; ndestruct;
@@ -40 +40 @@
   
 (* The size checking rejects the read and gives us Some Vundef. *)
-nremark vl_undef: load Mint16signed store3 block 0 = Some ? Vundef. //; nqed.
+nremark vl_undef: load Mint16signed store3 Any block 0 = Some ? Vundef. //; nqed.
 
 (* The read is successful and returns a signed version of the value. *)
-nremark vl_ok': load Mint8unsigned store3 block 0 = Some ? (Vint (zero_ext 8 one)). //; nqed.
+nremark vl_ok': load Mint8unsigned store3 Any block 0 = Some ? (Vint (zero_ext 8 one)). //; nqed.
 
 (* NB: Double frees are allowed by the memory model (although not necessarily
@@ -53 +53 @@
    stack memory in the semantics. *)
 ndefinition storeA := empty.
-ndefinition storeBblkB := alloc storeA 0 4.
-ndefinition storeCblkC := alloc (fst ?? storeBblkB) 0 8.
+ndefinition storeBblkB := alloc storeA 0 4 Any.
+ndefinition storeCblkC := alloc (fst ?? storeBblkB) 0 8 Any.
 ndefinition storeD := free (fst ?? storeCblkC) (snd ?? storeBblkB).
 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. *)
 ndefinition storeI := empty.
-ndefinition storeIIblk := alloc storeA 0 4.
+ndefinition storeIIblk := alloc storeA 0 4 Any.
 ndefinition storeIII : mem.
- nletin r ≝ (store Mint32 (fst ?? storeIIblk) (snd ?? storeIIblk) 0 (Vint one));
+ nletin r ≝ (store Mint32 (fst ?? storeIIblk) Any (snd ?? storeIIblk) 0 (Vint one));
   nlapply (refl ? r); nelim r in ⊢ (???% → ?);##[ nwhd in ⊢ (??%? → ?); #H; ndestruct;
   ##| #rr; #_; napply rr ##] nqed.
-ndefinition byte := load Mint8unsigned storeIII (snd ?? storeIIblk) 0.
+ndefinition byte := load Mint8unsigned storeIII Any (snd ?? storeIIblk) 0.
 nremark byteundef: byte = Some ? Vundef. //; nqed. (* :( *)