Ignore:
Timestamp:
Jan 4, 2013, 2:59:37 PM (7 years ago)
Author:
campbell
Message:

Fix Clight semantics for ptr + char. (Compiler works anyway.)

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/toCminorCorrectness.ma

    r2568 r2569  
    608608  sem_add v1 (Tint sz sg) v2 (ptr_type ty' optlen) = Some ? res →
    609609  ∃sz',i. v1 = Vint sz' i ∧
    610       ((∃p. v2 = Vptr p ∧ res = Vptr (shift_pointer_n ? p (sizeof ty') i)) ∨
     610      ((∃p. v2 = Vptr p ∧ res = Vptr (shift_pointer_n ? p (sizeof ty') sg i)) ∨
    611611       (v2 = Vnull ∧ i = (zero ?) ∧ res = Vnull)).
    612612#tsz #tsg #ty' * [ | #n ]
     
    637637  sem_add v1 (ptr_type ty' optlen) v2 (Tint sz sg) = Some ? res →
    638638  ∃sz',i. v2 = Vint sz' i ∧
    639       ((∃p. v1 = Vptr p ∧ res = Vptr (shift_pointer_n ? p (sizeof ty') i)) ∨
     639      ((∃p. v1 = Vptr p ∧ res = Vptr (shift_pointer_n ? p (sizeof ty') sg i)) ∨
    640640       (v1 = Vnull ∧ i = (zero ?) ∧ res = Vnull)).
    641641#tsz #tsg #ty' * [ | #n ]
Note: See TracChangeset for help on using the changeset viewer.