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/Cminor/initialisation.ma

    r887 r961  
    99λinit.
    1010match init return λ_.option (Σc:memory_chunk. expr (typ_of_memory_chunk c)) with
    11 [ Init_int8 i          ⇒ Some ? (dp ?? Mint8unsigned (Cst ? (Ointconst i)))
    12 | Init_int16 i         ⇒ Some ? (dp ?? Mint16unsigned (Cst ? (Ointconst i)))
    13 | Init_int32 i         ⇒ Some ? (dp ?? Mint32 (Cst ? (Ointconst i)))
     11[ Init_int8 i          ⇒ Some ? (dp ?? Mint8unsigned (Cst ? (Ointconst I8 i)))
     12| Init_int16 i         ⇒ Some ? (dp ?? Mint16unsigned (Cst ? (Ointconst I16 i)))
     13| Init_int32 i         ⇒ Some ? (dp ?? Mint32 (Cst ? (Ointconst I32 i)))
    1414| Init_float32 f       ⇒ Some ? (dp ?? Mfloat32 (Cst ? (Ofloatconst f)))
    1515| Init_float64 f       ⇒ Some ? (dp ?? Mfloat64 (Cst ? (Ofloatconst f)))
    1616| Init_space n         ⇒ None ?
    17 | Init_null r          ⇒ Some ? (dp ?? (Mpointer r) (Op1 (ASTint I8 Unsigned) ? (Optrofint r) (Cst ? (Ointconst zero))))
     17| Init_null r          ⇒ Some ? (dp ?? (Mpointer r) (Op1 (ASTint I8 Unsigned) ? (Optrofint r) (Cst ? (Ointconst I8 (zero ?)))))
    1818| Init_addrof r id off ⇒ Some ? (dp ?? (Mpointer r) (Cst ? (Oaddrsymbol id off)))
    1919].
     
    2222   away. *)
    2323
    24 definition init_datum : ident → region → init_data → int (*offset?*) → stmt ≝
     24definition init_datum : ident → region → init_data → nat (*offset*) → stmt ≝
    2525λid,r,init,off.
    2626match init_expr init with
     
    3737  (λdatum,os.
    3838   let 〈off,s〉 ≝ os in
    39      〈addition_n ? off (repr (size_init_data datum)), St_seq (init_datum id r datum off) s〉)
    40   〈zero, St_skip〉 init).
     39     〈off + (size_init_data datum), St_seq (init_datum id r datum off) s〉)
     40  〈0, St_skip〉 init).
    4141
    4242definition init_vars : list (ident × (list init_data) × region × unit) → stmt ≝
Note: See TracChangeset for help on using the changeset viewer.