Changeset 961 for src/Cminor/initialisation.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/Cminor/initialisation.ma (modified) (3 diffs)

src/Cminor/initialisation.ma

@@ -9 +9 @@
 λinit.
 match init return λ_.option (Σc:memory_chunk. expr (typ_of_memory_chunk c)) with
-[ Init_int8 i          ⇒ Some ? (dp ?? Mint8unsigned (Cst ? (Ointconst i)))
-| Init_int16 i         ⇒ Some ? (dp ?? Mint16unsigned (Cst ? (Ointconst i)))
-| Init_int32 i         ⇒ Some ? (dp ?? Mint32 (Cst ? (Ointconst i)))
+[ Init_int8 i          ⇒ Some ? (dp ?? Mint8unsigned (Cst ? (Ointconst I8 i)))
+| Init_int16 i         ⇒ Some ? (dp ?? Mint16unsigned (Cst ? (Ointconst I16 i)))
+| Init_int32 i         ⇒ Some ? (dp ?? Mint32 (Cst ? (Ointconst I32 i)))
 | Init_float32 f       ⇒ Some ? (dp ?? Mfloat32 (Cst ? (Ofloatconst f)))
 | Init_float64 f       ⇒ Some ? (dp ?? Mfloat64 (Cst ? (Ofloatconst f)))
 | Init_space n         ⇒ None ?
-| Init_null r          ⇒ Some ? (dp ?? (Mpointer r) (Op1 (ASTint I8 Unsigned) ? (Optrofint r) (Cst ? (Ointconst zero))))
+| Init_null r          ⇒ Some ? (dp ?? (Mpointer r) (Op1 (ASTint I8 Unsigned) ? (Optrofint r) (Cst ? (Ointconst I8 (zero ?)))))
 | Init_addrof r id off ⇒ Some ? (dp ?? (Mpointer r) (Cst ? (Oaddrsymbol id off)))
 ].
@@ -22 +22 @@
    away. *)
 
-definition init_datum : ident → region → init_data → int (*offset?*) → stmt ≝
+definition init_datum : ident → region → init_data → nat (*offset*) → stmt ≝
 λid,r,init,off.
 match init_expr init with
@@ -37 +37 @@
   (λdatum,os.
    let 〈off,s〉 ≝ os in
-     〈addition_n ? off (repr (size_init_data datum)), St_seq (init_datum id r datum off) s〉)
-  〈zero, St_skip〉 init).
+     〈off + (size_init_data datum), St_seq (init_datum id r datum off) s〉)
+  〈0, St_skip〉 init).
 
 definition init_vars : list (ident × (list init_data) × region × unit) → stmt ≝