Changeset 718 for src/common/Mem.ma


Ignore:
Timestamp:
Mar 29, 2011, 5:54:37 PM (10 years ago)
Author:
campbell
Message:

Add an AST type (i.e., intermediate language type) for pointers.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/Mem.ma

    r700 r718  
    127127  encoding the type, size and signedness of the chunk being addressed.
    128128  The following functions extract the size information from a chunk. *)
    129 
    130 definition size_pointer : region → Z ≝
    131 λsp. match sp return λ_.Z with [ Data ⇒ 1 | IData ⇒ 1 | PData ⇒ 1 | XData ⇒ 2 | Code ⇒ 2 | Any ⇒ 3 ].
    132129
    133130definition size_chunk : memory_chunk → Z ≝
Note: See TracChangeset for help on using the changeset viewer.