Changeset 156


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

pdata support

Location:
C-semantics
Files:
2 added
5 edited

Legend:

Unmodified
Added
Removed
  • C-semantics/AST.ma

    r153 r156  
    111111  | Data : memory_space
    112112  | IData : memory_space
     113  | PData : memory_space
    113114  | XData : memory_space
    114115  | Code : memory_space.
  • C-semantics/CexecIO.ma

    r155 r156  
    838838napply opt_bindIO_OK; #u ecode;
    839839napply opt_bindIO_OK; #f ef;
    840 ncases sp in esb ecode; #esb ecode; nwhd in ecode:(??%%); ##[ ##1,2,3,4: ndestruct (ecode); ##]
     840ncases sp in esb ecode; #esb ecode; nwhd in ecode:(??%%); ##[ ##1,2,3,4,5: ndestruct (ecode); ##]
    841841nwhd; napply (initial_state_intro … esb ef);
    842842nqed.
  • 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
  • C-semantics/Mem.ma

    r153 r156  
    559559
    560560ninductive pointer_compat : memory_space → memory_space → Prop ≝
    561 |  data_compat : pointer_compat  Data  Data
    562 | idata_compat : pointer_compat IData IData
    563 | xdata_compat : pointer_compat XData XData
    564 |  code_compat : pointer_compat  Code  Code
     561|  same_compat : ∀s. pointer_compat s s
     562| pxdata_compat : pointer_compat PData XData
    565563| unspecified_compat : ∀p. pointer_compat Any p
    566564| universal_compat : ∀b. pointer_compat b Any.
  • C-semantics/Values.ma

    r153 r156  
    417417    | Data ⇒ match chunk with [ Mint8unsigned ⇒ Vptr pty b ofs | _ ⇒ Vundef ]
    418418    | IData ⇒ match chunk with [ Mint8unsigned ⇒ Vptr pty b ofs | _ ⇒ Vundef ]
     419    | PData ⇒ match chunk with [ Mint8unsigned ⇒ Vptr pty b ofs | _ ⇒ Vundef ]
    419420    | XData ⇒ match chunk with [ Mint16unsigned ⇒ Vptr pty b ofs | _ ⇒ Vundef ]
    420421    | Code ⇒ match chunk with [ Mint16unsigned ⇒ Vptr pty b ofs | _ ⇒ Vundef ]
Note: See TracChangeset for help on using the changeset viewer.