Ignore:
Timestamp:
Jun 3, 2011, 5:35:31 PM (8 years ago)
Author:
campbell
Message:

Add type information into Cminor.
As a result, the Clight to Cminor stage now does extra type checking.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Cminor/initialisation.ma

    r758 r880  
    55include "common/Globalenvs.ma".
    66
    7 definition init_expr : init_data → option (memory_chunk × expr) ≝
     7(* XXX having to specify the return type in the match is annoying. *)
     8definition init_expr : init_data → option (Σc:memory_chunk. expr (typ_of_memory_chunk c)) ≝
    89λinit.
    9 match init with
    10 [ Init_int8 i          ⇒ Some ? 〈Mint8unsigned, Cst (Ointconst i)〉
    11 | Init_int16 i         ⇒ Some ? 〈Mint16unsigned, Cst (Ointconst i)〉
    12 | Init_int32 i         ⇒ Some ? 〈Mint32, Cst (Ointconst i)〉
    13 | Init_float32 f       ⇒ Some ? 〈Mfloat32, Cst (Ofloatconst f)〉
    14 | Init_float64 f       ⇒ Some ? 〈Mfloat64, Cst (Ofloatconst f)〉
     10match 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)))
     14| Init_float32 f       ⇒ Some ? (dp ?? Mfloat32 (Cst ? (Ofloatconst f)))
     15| Init_float64 f       ⇒ Some ? (dp ?? Mfloat64 (Cst ? (Ofloatconst f)))
    1516| Init_space n         ⇒ None ?
    16 | Init_null r          ⇒ Some ? 〈Mpointer r, Op1 (Optrofint r) (Cst (Ointconst zero))〉
    17 | Init_addrof r id off ⇒ Some ? 〈Mpointer r, Cst (Oaddrsymbol id off)〉
     17| Init_null r          ⇒ Some ? (dp ?? (Mpointer r) (Op1 (ASTint I8 Unsigned) ? (Optrofint r) (Cst ? (Ointconst zero))))
     18| Init_addrof r id off ⇒ Some ? (dp ?? (Mpointer r) (Cst ? (Oaddrsymbol id off)))
    1819].
    1920
     
    2627[ None ⇒ St_skip
    2728| Some x ⇒
    28     let 〈chunk, e〉 ≝ x in
    29     St_store chunk (Cst (Oaddrsymbol id off)) e
     29    match x with [ dp chunk e ⇒
     30      St_store ? chunk (Cst ? (Oaddrsymbol id off)) e
     31    ]
    3032].
    3133
Note: See TracChangeset for help on using the changeset viewer.