Changeset 156 for C-semantics/Csyntax.ma


Ignore:
Timestamp:
Oct 6, 2010, 4:17:57 PM (10 years ago)
Author:
campbell
Message:

pdata support

File:
1 edited

Legend:

Unmodified
Added
Removed
  • C-semantics/Csyntax.ma

    r153 r156  
    438438
    439439ndefinition sizeof_pointer : memory_space → Z ≝
    440 λsp. match sp with [ Data ⇒ 1 | IData ⇒ 1 | XData ⇒ 2 | Code ⇒ 2 | Any ⇒ 3 ].
     440λsp. match sp with [ Data ⇒ 1 | IData ⇒ 1 | PData ⇒ 1 | XData ⇒ 2 | Code ⇒ 2 | Any ⇒ 3 ].
    441441
    442442nlet rec sizeof (t: type) : Z ≝
     
    634634                            | F64 ⇒ By_value Mfloat64 ]
    635635  | Tvoid ⇒ By_nothing
    636   | Tpointer sp _ ⇒ By_value (match sp with [ Any ⇒ Mint24 | Data ⇒ Mint8unsigned | IData ⇒ Mint8unsigned | XData ⇒ Mint16unsigned | Code ⇒ Mint16unsigned ])
     636  | Tpointer sp _ ⇒ By_value (match sp with [ Any ⇒ Mint24 | Data ⇒ Mint8unsigned | IData ⇒ Mint8unsigned | PData ⇒ Mint8unsigned | XData ⇒ Mint16unsigned | Code ⇒ Mint16unsigned ])
    637637  | Tarray _ _ _ ⇒ By_reference
    638638  | Tfunction _ _ ⇒ By_reference
Note: See TracChangeset for help on using the changeset viewer.