Changeset 2569 for src/Clight/Csem.ma


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

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

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/Csem.ma

    r2560 r2569  
    110110        | _ ⇒ None ? ]
    111111      | _ ⇒ None ? ]
    112   | add_case_pi _ ty _ _ ⇒                    (**r pointer plus integer *)
     112  | add_case_pi _ ty _ sg ⇒                    (**r pointer plus integer *)
    113113      match v1 with
    114114      [ Vptr ptr1 ⇒ match v2 with
    115         [ Vint sz2 n2 ⇒ Some ? (Vptr (shift_pointer_n ? ptr1 (sizeof ty) n2))
     115        [ Vint sz2 n2 ⇒ Some ? (Vptr (shift_pointer_n ? ptr1 (sizeof ty) sg n2))
    116116        | _ ⇒ None ? ]
    117117      | Vnull ⇒ match v2 with
     
    119119        | _ ⇒ None ? ]
    120120      | _ ⇒ None ? ]
    121   | add_case_ip _ _ _ ty ⇒                    (**r integer plus pointer *)
     121  | add_case_ip _ _ sg ty ⇒                    (**r integer plus pointer *)
    122122      match v1 with
    123123      [ Vint sz1 n1 ⇒ match v2 with
    124         [ Vptr ptr2 ⇒ Some ? (Vptr (shift_pointer_n ? ptr2 (sizeof ty) n1))
     124        [ Vptr ptr2 ⇒ Some ? (Vptr (shift_pointer_n ? ptr2 (sizeof ty) sg n1))
    125125        | Vnull ⇒ if eq_bv ? n1 (zero ?) then Some ? Vnull else None ?
    126126        | _ ⇒ None ? ]
     
    138138        | _ ⇒ None ? ]
    139139      | _ ⇒ None ? ]
    140   | sub_case_pi _ ty _ _ ⇒             (**r pointer minus integer *)
     140  | sub_case_pi _ ty _ sg ⇒             (**r pointer minus integer *)
    141141      match v1 with
    142142      [ Vptr ptr1 ⇒ match v2 with
    143         [ Vint sz2 n2 ⇒ Some ? (Vptr (neg_shift_pointer_n ? ptr1 (sizeof ty) n2))
     143        [ Vint sz2 n2 ⇒ Some ? (Vptr (neg_shift_pointer_n ? ptr1 (sizeof ty) sg n2))
    144144        | _ ⇒ None ? ]
    145145      | Vnull ⇒ match v2 with
Note: See TracChangeset for help on using the changeset viewer.