Ignore:
Timestamp:
Jan 28, 2011, 2:41:48 PM (8 years ago)
Author:
campbell
Message:

Use pointer-specific "chunks" of memory for pointer loads and stores,
in particular getting rid of Mint24.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.1/C-semantics/Csyntax.ma

    r481 r483  
    631631  | By_nothing: mode.
    632632
    633 ndefinition access_mode_pointer : region → mode ≝ λr.
    634 By_value (match r with
    635 [ Any   ⇒ Mint24
    636 | Data  ⇒ Mint8unsigned
    637 | IData ⇒ Mint8unsigned
    638 | PData ⇒ Mint8unsigned
    639 | XData ⇒ Mint16unsigned
    640 | Code ⇒ Mint16unsigned
    641 ]).
    642 
    643633ndefinition access_mode : type → mode ≝ λty.
    644634  match ty with
     
    654644                            | F64 ⇒ By_value Mfloat64 ]
    655645  | Tvoid ⇒ By_nothing
    656   | Tpointer r _ ⇒ access_mode_pointer r
     646  | Tpointer r _ ⇒ By_value (Mpointer r)
    657647  | Tarray _ _ _ ⇒ By_reference
    658648  | Tfunction _ _ ⇒ By_reference
    659649  | Tstruct _ fList ⇒ By_nothing
    660650  | Tunion _ fList ⇒ By_nothing
    661   | Tcomp_ptr r _ ⇒ access_mode_pointer r
     651  | Tcomp_ptr r _ ⇒ By_value (Mpointer r)
    662652  ].
    663653
Note: See TracChangeset for help on using the changeset viewer.