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/CexecComplete.ma

    r468 r481  
    267267  (st:∀i,fl. P (Tstruct i fl))
    268268  (un:∀i,fl. P (Tunion i fl))
    269   (cp:∀i. P (Tcomp_ptr i))
     269  (cp:∀r,i. P (Tcomp_ptr r i))
    270270  (nl:Q Tnil)
    271271  (cs:∀t,tl. P t → Q tl → Q (Tcons t tl))
     
    280280  | Tstruct i fs ⇒ st i fs
    281281  | Tunion i fs ⇒ un i fs
    282   | Tcomp_ptr i ⇒ cp i
     282  | Tcomp_ptr r i ⇒ cp r i
    283283  ]
    284284and typelist_ind2l
     
    292292  (st:∀i,fl. P (Tstruct i fl))
    293293  (un:∀i,fl. P (Tunion i fl))
    294   (cp:∀i. P (Tcomp_ptr i))
     294  (cp:∀r,i. P (Tcomp_ptr r i))
    295295  (nl:Q Tnil)
    296296  (cs:∀t,tl. P t → Q tl → Q (Tcons t tl))
Note: See TracChangeset for help on using the changeset viewer.