Ignore:
Timestamp:
Jan 28, 2011, 2:41:48 PM (9 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/Values.ma

    r482 r483  
    407407    | Mint16signed ⇒ Vint (sign_ext 16 n)
    408408    | Mint16unsigned ⇒ Vint (zero_ext 16 n)
    409     | Mint24 ⇒ Vint (zero_ext 24 n)
    410409    | Mint32 ⇒ Vint n
     410    | Mpointer r ⇒ if eq n zero then Vint zero else Vundef
    411411    | _ ⇒ Vundef
    412412    ]
    413   | Vptr pty b ofs ⇒
    414     match pty with
    415     [ Any ⇒ match chunk with [ Mint24 ⇒ Vptr pty b ofs | _ ⇒ Vundef ]
    416     | Data ⇒ match chunk with [ Mint8unsigned ⇒ Vptr pty b ofs | _ ⇒ Vundef ]
    417     | IData ⇒ match chunk with [ Mint8unsigned ⇒ Vptr pty b ofs | _ ⇒ Vundef ]
    418     | PData ⇒ 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 ]
     413  | Vptr r b ofs ⇒
     414    match chunk with
     415    [ Mpointer r' ⇒ if eq_region r r' then Vptr r b ofs else Vundef
     416    | _ ⇒ Vundef
    421417    ]
    422418  | Vfloat f ⇒
     
    10131009  ∀chunk,v1,v2.
    10141010  Val_lessdef v1 v2 → Val_lessdef (load_result chunk v1) (load_result chunk v2).
    1015 #chunk;#v1;#v2;#H; ninversion H; //; #v e1 e2; ncases chunk; nwhd in ⊢ (?%?); //;
     1011#chunk;#v1;#v2;#H; ninversion H; //; #v e1 e2; ncases chunk;
     1012##[ ##8: #r ##] nwhd in ⊢ (?%?); //;
    10161013nqed.
    10171014
Note: See TracChangeset for help on using the changeset viewer.