Changeset 961 for src/Cminor/initialisation.ma
- Timestamp:
- Jun 15, 2011, 4:15:52 PM (10 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/Cminor/initialisation.ma
r887 r961 9 9 λinit. 10 10 match 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))) 14 14 | Init_float32 f ⇒ Some ? (dp ?? Mfloat32 (Cst ? (Ofloatconst f))) 15 15 | Init_float64 f ⇒ Some ? (dp ?? Mfloat64 (Cst ? (Ofloatconst f))) 16 16 | 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 ?))))) 18 18 | Init_addrof r id off ⇒ Some ? (dp ?? (Mpointer r) (Cst ? (Oaddrsymbol id off))) 19 19 ]. … … 22 22 away. *) 23 23 24 definition init_datum : ident → region → init_data → int (*offset?*) → stmt ≝24 definition init_datum : ident → region → init_data → nat (*offset*) → stmt ≝ 25 25 λid,r,init,off. 26 26 match init_expr init with … … 37 37 (λdatum,os. 38 38 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). 41 41 42 42 definition init_vars : list (ident × (list init_data) × region × unit) → stmt ≝
Note: See TracChangeset
for help on using the changeset viewer.