Ignore:
Timestamp:
Jul 12, 2012, 1:28:28 PM (7 years ago)
Author:
campbell
Message:

Remove memory spaces other than XData and Code; simplify pointers as a
result.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Cminor/initialisation.ma

    r1878 r2176  
    1515| Init_float64 f       ⇒ Some ? (mk_DPair ?? (ASTfloat F64) (Cst ? (Ofloatconst F64 f)))
    1616| Init_space n         ⇒ None ?
    17 | Init_null r          ⇒ Some ? (mk_DPair ?? (ASTptr r) (Op1 (ASTint I8 Unsigned) ? (Optrofint ?? r) (Cst ? (Ointconst I8 Unsigned (zero ?)))))
    18 | Init_addrof r id off ⇒ Some ? (mk_DPair ?? (ASTptr r) (Cst ? (Oaddrsymbol r id off)))
     17| Init_null            ⇒ Some ? (mk_DPair ?? ASTptr (Op1 (ASTint I8 Unsigned) ? (Optrofint ??) (Cst ? (Ointconst I8 Unsigned (zero ?)))))
     18| Init_addrof   id off ⇒ Some ? (mk_DPair ?? ASTptr (Cst ? (Oaddrsymbol id off)))
    1919].
    2020
     
    3535| Some x ⇒
    3636    match x with [ mk_DPair t e ⇒
    37       St_store t r (Cst ? (Oaddrsymbol r id off)) e
     37      St_store t (Cst ? (Oaddrsymbol id off)) e
    3838    ]
    3939].
    4040% //
    41 cases init in p; [ 8: #a #b ] #c #p normalize in p;
     41cases init in p; [ 7: | 8: #a #b | *: #a ] #p normalize in p;
    4242destruct;/2/
    4343qed.
Note: See TracChangeset for help on using the changeset viewer.