Changeset 2176 for src/Clight/test/memorymodel.ma

Timestamp:

Jul 12, 2012, 1:28:28 PM (8 years ago)

Author:

campbell

Message:

Remove memory spaces other than XData and Code; simplify pointers as a
result.

File:

• src/Clight/test/memorymodel.ma (modified) (6 diffs)

src/Clight/test/memorymodel.ma

@@ -21 +21 @@
    store. *)
 definition store0 := empty.
-definition store1block : mem × Σb:block.? ≝ alloc store0 0 4 Any.
+definition store1block : mem × Σb:block.? ≝ alloc store0 0 4 XData.
 definition store1 : mem ≝ fst ?? store1block.
 definition block :block := pi1 … (snd ?? store1block).
@@ -27 +27 @@
 (* write a value *)
 definition store2 : mem.
-  letin r ≝ (store (ASTint I16 Unsigned) store1 (mk_pointer Any block (same_compat …) zero_offset) (Vint I16 (repr ? 1)));
+  letin r ≝ (store (ASTint I16 Unsigned) store1 (mk_pointer block zero_offset) (Vint I16 (repr ? 1)))
 
   lapply (refl ? r); elim r in ⊢ (???% → ?); [ whd in ⊢ (??%? → ?); #H destruct
@@ -34 +34 @@
 (* overwrite the first byte of the value *)
 definition store3 : mem.
-  letin r ≝ (store (ASTint I8 Unsigned) store2 (mk_pointer Any block (same_compat …) zero_offset) (Vint I8 (repr ? 1)));
+  letin r ≝ (store (ASTint I8 Unsigned) store2 (mk_pointer block zero_offset) (Vint I8 (repr ? 1)))
 
   lapply (refl ? r) elim r in ⊢ (???% → ?); [ whd in ⊢ (??%? → ?); #H destruct
@@ -41 +41 @@
 (* This is what happened under the original CompCert 1.6 ported memory model:
    The size checking rejects the read and gives us Some Vundef.
-example vl_undef: load (ASTint I16 Signed) store3 (mk_pointer Any block (same_compat …) zero_offset) = Some ? Vundef. @refl qed.
+example vl_undef: load (ASTint I16 Signed) store3 (mk_pointer block zero_offset) = Some ? Vundef. @refl qed.
 *)
 (* Now we do byte-wise values and get to see the altered integer. *)
-example vl_changed: load (ASTint I16 Signed) store3 (mk_pointer Any block (same_compat …) zero_offset) = Some ? (Vint I16 (repr ? 257)). @refl qed.
+example vl_changed: load (ASTint I16 Signed) store3 (mk_pointer block zero_offset) = Some ? (Vint I16 (repr ? 257)). @refl qed.
 
 (* The read is successful and returns the value. *)
-example vl_ok': load (ASTint I8 Unsigned) store3 (mk_pointer Any block (same_compat …) zero_offset) = Some ? (Vint I8 (repr ? 1)). // qed.
+example vl_ok': load (ASTint I8 Unsigned) store3 (mk_pointer block zero_offset) = Some ? (Vint I8 (repr ? 1)). // qed.
 
 (* NB: Double frees are allowed by the memory model (although not necessarily
@@ -57 +57 @@
    stack memory in the semantics. *)
 definition storeA := empty.
-definition storeBblkB := alloc storeA 0 4 Any.
-definition storeCblkC := alloc (fst ?? storeBblkB) 0 8 Any.
+definition storeBblkB := alloc storeA 0 4 XData.
+definition storeCblkC := alloc (fst ?? storeBblkB) 0 8 XData.
 definition storeD := free (fst ?? storeCblkC) (snd ?? storeBblkB).
 definition storeE : mem. letin r ≝ (free storeD (snd ?? storeCblkC)).
@@ -67 +67 @@
    doesn't currently expose parts of pointers. *)
 definition storeI := empty.
-definition storeIIblk := alloc storeI 0 4 Any.
+definition storeIIblk := alloc storeI 0 4 XData.
 definition storeIII : mem.
- letin r ≝ (store (ASTint I32 Unsigned) (fst ?? storeIIblk) (mk_pointer Any (snd ?? storeIIblk) (same_compat …) zero_offset) (Vint I32 (repr ? 1)));
+ letin r ≝ (store (ASTint I32 Unsigned) (fst ?? storeIIblk) (mk_pointer (snd ?? storeIIblk) zero_offset) (Vint I32 (repr ? 1)));
   lapply (refl ? r) elim r in ⊢ (???% → ?); [ whd in ⊢ (??%? → ?); #H destruct
   | #rr #_ @rr ] qed.
-definition byte := load (ASTint I8 Unsigned) storeIII (mk_pointer Any (snd ?? storeIIblk) (same_compat …) zero_offset).
+definition byte := load (ASTint I8 Unsigned) storeIII (mk_pointer (snd ?? storeIIblk) zero_offset).
 example byteundef: byte = Some ? (Vint I8 (repr ? 0)). // qed. (* :) *)
+