Changeset 1988 for src/Clight/test

Timestamp:

May 24, 2012, 11:39:27 AM (9 years ago)

Author:

campbell

Message:

Abstraction of the memory contents in the memory models is no longer
necessary.

File:

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

src/Clight/test/memorymodel.ma

@@ -20 +20 @@
    access, preventing you reading back more information than the memory can
    store. *)
-definition store0 := empty becontentT.
-definition store1block : mem × Σb:block.? ≝ alloc ? store0 0 4 Any.
+definition store0 := empty.
+definition store1block : mem × Σb:block.? ≝ alloc store0 0 4 Any.
 definition store1 : mem ≝ fst ?? store1block.
 definition block :block := pi1 … (snd ?? store1block).
@@ -51 +51 @@
 (* NB: Double frees are allowed by the memory model (although not necessarily
        by the language). *)
-definition store4 := free ? store3 block.
-definition store5 : mem. letin r ≝ (free ? store3 block); whd in r; @r qed.
+definition store4 := free store3 block.
+definition store5 : mem. letin r ≝ (free store3 block); whd in r; @r qed.
 
 (* No ordering is imposed on deallocation (even though alloc and free are only used for
    stack memory in the semantics. *)
-definition storeA := empty becontentT.
-definition storeBblkB := alloc ? storeA 0 4 Any.
-definition storeCblkC := alloc ? (fst ?? storeBblkB) 0 8 Any.
-definition storeD := free ? (fst ?? storeCblkC) (snd ?? storeBblkB).
-definition storeE : mem. letin r ≝ (free ? storeD (snd ?? storeCblkC)).
+definition storeA := empty.
+definition storeBblkB := alloc storeA 0 4 Any.
+definition storeCblkC := alloc (fst ?? storeBblkB) 0 8 Any.
+definition storeD := free (fst ?? storeCblkC) (snd ?? storeBblkB).
+definition storeE : mem. letin r ≝ (free storeD (snd ?? storeCblkC)).
 whd in r; @r qed.
 
@@ -66 +66 @@
    but can now split up integer values into bytes.  The front-end interface
    doesn't currently expose parts of pointers. *)
-definition storeI := empty becontentT.
-definition storeIIblk := alloc ? storeA 0 4 Any.
+definition storeI := empty.
+definition storeIIblk := alloc storeI 0 4 Any.
 definition storeIII : mem.
  letin r ≝ (store (ASTint I32 Unsigned) (fst ?? storeIIblk) (mk_pointer Any (snd ?? storeIIblk) (same_compat …) zero_offset) (Vint I32 (repr ? 1)));