Ignore:
Timestamp:
Jan 25, 2011, 6:22:21 PM (9 years ago)
Author:
campbell
Message:

Tcomp_ptr should take the memory region and use that to calculate its size.

File:
1 edited

Legend:

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

    r480 r481  
    422422    | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
    423423    |  _ ⇒ inr ?? (nmk ? (λH.?)) ]
    424 | Tcomp_ptr i ⇒ match t2 return λt'. (Tcomp_ptr ? = t') + (Tcomp_ptr ? ≠ t')  with [ Tcomp_ptr i' ⇒
    425     match ident_eq i i' with [ inl e1 ⇒ inl ???
     424| Tcomp_ptr r i ⇒ match t2 return λt'. (Tcomp_ptr ? ? = t') + (Tcomp_ptr ? ? ≠ t')  with [ Tcomp_ptr r' i' ⇒
     425    match ms_eq_dec r r' with [ inl e1 ⇒
     426      match ident_eq i i' with [ inl e2 ⇒ inl ???
     427      | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
    426428    | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
    427429    | _ ⇒ inr ?? (nmk ? (λH.?)) ]
Note: See TracChangeset for help on using the changeset viewer.