Changeset 153


Ignore:
Timestamp:
Oct 6, 2010, 2:20:25 PM (9 years ago)
Author:
campbell
Message:

Use appropriate memory chunks for 8051 pointers.

Location:
C-semantics
Files:
4 edited

Legend:

Unmodified
Added
Removed
  • C-semantics/AST.ma

    r125 r153  
    100100  | Mint16signed : memory_chunk    (*r 16-bit signed integer *)
    101101  | Mint16unsigned : memory_chunk  (*r 16-bit unsigned integer *)
     102  | Mint24 : memory_chunk
    102103  | Mint32 : memory_chunk          (*r 32-bit integer, or pointer *)
    103104  | Mfloat32 : memory_chunk        (*r 32-bit single-precision float *)
  • C-semantics/Csyntax.ma

    r127 r153  
    634634                            | F64 ⇒ By_value Mfloat64 ]
    635635  | Tvoid ⇒ By_nothing
    636   | Tpointer _ _ ⇒ By_value Mint32
     636  | Tpointer sp _ ⇒ By_value (match sp with [ Any ⇒ Mint24 | Data ⇒ Mint8unsigned | IData ⇒ Mint8unsigned | XData ⇒ Mint16unsigned | Code ⇒ Mint16unsigned ])
    637637  | Tarray _ _ _ ⇒ By_reference
    638638  | Tfunction _ _ ⇒ By_reference
  • C-semantics/Mem.ma

    r125 r153  
    116116  | Mint16signed => 2
    117117  | Mint16unsigned => 2
     118  | Mint24 ⇒ 3
    118119  | Mint32 => 4
    119120  | Mfloat32 => 4
     
    126127  | Mint16signed => 1
    127128  | Mint16unsigned => 1
     129  | Mint24 ⇒ 2
    128130  | Mint32 => 3
    129131  | Mfloat32 => 3
     
    156158  [ Mint8signed ⇒ 1
    157159  | Mint8unsigned ⇒ 1
    158   | Mint16signed ⇒ 2
    159   | Mint16unsigned ⇒ 2
    160   | _ ⇒ 4 ].
     160  | Mint16signed ⇒ 1
     161  | Mint16unsigned ⇒ 1
     162  | _ ⇒ 1 ].
    161163
    162164nlemma align_chunk_pos:
     
    36103612#H; nwhd in ⊢ (??%%);
    36113613nelim (getN 0 (signed ofs) (contents (blocks m b)));
    3612 ##[ ##1,3,4: //;
     3614##[ ##1,3: //;
    36133615##| #i; nwhd in ⊢ (??(??%)(??%));
    36143616    nrewrite > (sign_ext_zero_ext ?? i); ##[ napply refl; (* XXX: // ? *)
    36153617    ##| (* arith *) napply daemon;
    36163618    ##]
     3619##| #sp; ncases sp; //;
    36173620##]
    36183621nqed.
  • C-semantics/Values.ma

    r125 r153  
    413413    ]
    414414  | Vptr pty b ofs ⇒
    415     match chunk with
    416     [ Mint32 ⇒ Vptr pty b ofs
    417     | _ ⇒ Vundef
     415    match pty with
     416    [ Any ⇒ match chunk with [ Mint24 ⇒ Vptr pty b ofs | _ ⇒ Vundef ]
     417    | Data ⇒ match chunk with [ Mint8unsigned ⇒ Vptr pty b ofs | _ ⇒ Vundef ]
     418    | IData ⇒ match chunk with [ Mint8unsigned ⇒ Vptr pty b ofs | _ ⇒ Vundef ]
     419    | XData ⇒ match chunk with [ Mint16unsigned ⇒ Vptr pty b ofs | _ ⇒ Vundef ]
     420    | Code ⇒ match chunk with [ Mint16unsigned ⇒ Vptr pty b ofs | _ ⇒ Vundef ]
    418421    ]
    419422  | Vfloat f ⇒
Note: See TracChangeset for help on using the changeset viewer.