Changeset 961 for src/common/Globalenvs.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/common/Globalenvs.ma (modified) (2 diffs)

src/common/Globalenvs.ma

@@ -406 +406 @@
   let r ≝ block_region m b in
   match id with
-  [ Init_int8 n ⇒ store Mint8unsigned m r b p (Vint n)
-  | Init_int16 n ⇒ store Mint16unsigned m r b p (Vint n)
-  | Init_int32 n ⇒ store Mint32 m r b p (Vint n)
+  [ Init_int8 n ⇒ store Mint8unsigned m r b p (Vint I8 n)
+  | Init_int16 n ⇒ store Mint16unsigned m r b p (Vint I16 n)
+  | Init_int32 n ⇒ store Mint32 m r b p (Vint I32 n)
   | Init_float32 n ⇒ store Mfloat32 m r b p (Vfloat n)
   | Init_float64 n ⇒ store Mfloat64 m r b p (Vfloat n)
@@ -416 +416 @@
       | Some b' ⇒ 
         match pointer_compat_dec b' r' with
-        [ inl pc ⇒ store (Mpointer r') m r b p (Vptr r' b' pc (shift_offset zero_offset ofs))
+        [ inl pc ⇒ store (Mpointer r') m r b p (Vptr r' b' pc (shift_offset ? zero_offset (repr I16 ofs)))
         | inr _ ⇒ None ?
         ]