Changeset 153 for C-semantics/Mem.ma


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

Use appropriate memory chunks for 8051 pointers.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • 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.
Note: See TracChangeset for help on using the changeset viewer.