Ignore:
Timestamp:
Feb 22, 2011, 4:23:13 PM (9 years ago)
Author:
campbell
Message:

Abstract pointer offsets a little, similar to the changes for the prototype
proposed in Bologna.

File:
1 edited

Legend:

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

    r500 r583  
    263263  ]
    264264]
    265 and exec_lvalue' (ge:genv) (en:env) (m:mem) (e':expr_descr) (ty:type) on e' : res (block × int × trace) ≝
     265and exec_lvalue' (ge:genv) (en:env) (m:mem) (e':expr_descr) (ty:type) on e' : res (block × offset × trace) ≝
    266266  match e' with
    267267  [ Evar id ⇒
    268268      match (get … id en) with
    269       [ None ⇒ do l ← opt_to_res ? (find_symbol ? ? ge id); OK ? 〈〈l,zero〉,E0〉 (* global *)
    270       | Some loc ⇒ OK ? 〈〈loc,zero〉,E0〉 (* local *)
     269      [ None ⇒ do l ← opt_to_res ? (find_symbol ? ? ge id); OK ? 〈〈l,zero_offset〉,E0〉 (* global *)
     270      | Some loc ⇒ OK ? 〈〈loc,zero_offset〉,E0〉 (* local *)
    271271      ]
    272272  | Ederef a ⇒
     
    281281          do 〈lofs,tr〉 ← exec_lvalue ge en m a;
    282282          do delta ← field_offset i fList;
    283           OK ? 〈〈\fst lofs,add (\snd lofs) (repr delta)〉,tr〉
     283          OK ? 〈〈\fst lofs,shift_offset (\snd lofs) (repr delta)〉,tr〉
    284284      | Tunion id fList ⇒
    285285          do 〈lofs,tr〉 ← exec_lvalue ge en m a;
     
    289289  | _ ⇒ Error ?
    290290  ]
    291 and exec_lvalue (ge:genv) (en:env) (m:mem) (e:expr) on e : res (block × int × trace) ≝
     291and exec_lvalue (ge:genv) (en:env) (m:mem) (e:expr) on e : res (block × offset × trace) ≝
    292292match e with [ Expr e' ty ⇒ exec_lvalue' ge en m e' ty ].
    293293
     
    332332      | cons v1 vl ⇒
    333333          do b ← opt_to_res ? (get … id e);
    334           do m1 ← opt_to_res ? (store_value_of_type ty m b zero v1);
     334          do m1 ← opt_to_res ? (store_value_of_type ty m b zero_offset v1);
    335335          exec_bind_parameters e m1 params' vl
    336336      ]
Note: See TracChangeset for help on using the changeset viewer.