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

Timestamp:

Jun 15, 2011, 4:15:52 PM (10 years ago)

Author:

campbell

Message:

Use precise bitvector sizes throughout the front end, rather than 32bits
everywhere.

File:

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

src/Clight/test/memorymodel.ma

@@ -27 +27 @@
 (* write a value *)
 definition store2 : mem.
-  letin r ≝ (store Mint16unsigned store1 Any block 0 (Vint one));
+  letin r ≝ (store Mint16unsigned store1 Any block 0 (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 Mint8unsigned store1 Any block 0 (Vint one));
+  letin r ≝ (store Mint8unsigned store1 Any block 0 (Vint I8 (repr ? 1)));
 
   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.
 
-(* The read is successful and returns a signed version of the value. *)
-example vl_ok': load Mint8unsigned store3 Any block 0 = Some ? (Vint (zero_ext 8 one)). // qed.
+(* The read is successful and returns the value. *)
+example vl_ok': load Mint8unsigned store3 Any block 0 = Some ? (Vint I8 (repr ? 1)). // qed.
 
 (* NB: Double frees are allowed by the memory model (although not necessarily
@@ -63 +63 @@
 definition storeIIblk := alloc storeA 0 4 Any.
 definition storeIII : mem.
- letin r ≝ (store Mint32 (fst ?? storeIIblk) Any (snd ?? storeIIblk) 0 (Vint one));
+ letin r ≝ (store Mint32 (fst ?? storeIIblk) Any (snd ?? storeIIblk) 0 (Vint I32 (repr ? 1)));
   lapply (refl ? r) elim r in ⊢ (???% → ?) [ whd in ⊢ (??%? → ?) #H destruct
   | #rr #_ @rr ] qed.