Ignore:
Timestamp:
Jun 15, 2011, 4:15:52 PM (8 years ago)
Author:
campbell
Message:

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

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/Globalenvs.ma

    r797 r961  
    406406  let r ≝ block_region m b in
    407407  match id with
    408   [ Init_int8 n ⇒ store Mint8unsigned m r b p (Vint n)
    409   | Init_int16 n ⇒ store Mint16unsigned m r b p (Vint n)
    410   | Init_int32 n ⇒ store Mint32 m r b p (Vint n)
     408  [ Init_int8 n ⇒ store Mint8unsigned m r b p (Vint I8 n)
     409  | Init_int16 n ⇒ store Mint16unsigned m r b p (Vint I16 n)
     410  | Init_int32 n ⇒ store Mint32 m r b p (Vint I32 n)
    411411  | Init_float32 n ⇒ store Mfloat32 m r b p (Vfloat n)
    412412  | Init_float64 n ⇒ store Mfloat64 m r b p (Vfloat n)
     
    416416      | Some b' ⇒
    417417        match pointer_compat_dec b' r' with
    418         [ inl pc ⇒ store (Mpointer r') m r b p (Vptr r' b' pc (shift_offset zero_offset ofs))
     418        [ inl pc ⇒ store (Mpointer r') m r b p (Vptr r' b' pc (shift_offset ? zero_offset (repr I16 ofs)))
    419419        | inr _ ⇒ None ?
    420420        ]
Note: See TracChangeset for help on using the changeset viewer.