Ignore:
Timestamp:
Feb 11, 2011, 4:45:37 PM (9 years ago)
Author:
campbell
Message:

pointer_compat is a little more natural if it takes that block rather than
the block's region.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.1/C-semantics/Csem.ma

    r498 r499  
    432432      type_region ty r →
    433433      type_region ty' r' →
    434       pointer_compat (block_region m b) r' →
     434      pointer_compat b r' →
    435435      cast m (Vptr r b ofs) ty ty' (Vptr r' b ofs)
    436436  | cast_ip_z: ∀m,sz,sg,ty',r.
Note: See TracChangeset for help on using the changeset viewer.