Ignore:
Timestamp:
Feb 11, 2011, 4:45:28 PM (9 years ago)
Author:
campbell
Message:

First pass at moving regions to block type.

File:
1 edited

Legend:

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

    r487 r496  
    170170         [ Tpointer s _ ⇒ OK ? s | Tarray s _ _ ⇒ OK ? s | Tfunction _ _ ⇒ OK ? Code
    171171         | _ ⇒ Error ? ];
    172     if is_pointer_compat (block_space m b) s'
     172    if is_pointer_compat (block_region m b) s'
    173173    then OK ? (Vptr s' b ofs)
    174174    else Error ?
     
    184184
    185185definition load_value_of_type' ≝
    186 λty,m,l. match l with [ pair pl ofs ⇒ match pl with [ pair psp loc ⇒
    187   load_value_of_type ty m psp loc ofs ] ].
     186λty,m,l. match l with [ pair pl ofs ⇒ match pl with [ pair r loc ⇒
     187  load_value_of_type ty m r loc ofs ] ].
    188188
    189189(* To make the evaluation of bare lvalue expressions invoke exec_lvalue with
     
    258258  [ Evar id ⇒
    259259      match (get … id en) with
    260       [ None ⇒ do 〈sp,l〉 ← opt_to_res ? (find_symbol ? ? ge id); OK ? 〈〈〈sp,l〉,zero〉,E0〉 (* global *)
     260      [ None ⇒ do 〈r,l〉 ← opt_to_res ? (find_symbol ? ? ge id); OK ? 〈〈〈r,〈r,l〉〉,zero〉,E0〉 (* global *)
    261261      | Some loc ⇒ OK ? 〈〈〈Any,loc〉,zero〉,E0〉 (* local *)
    262262      ]
     
    654654  do ge ← globalenv Genv ?? p;
    655655  do m0 ← init_mem Genv ?? p;
    656   do 〈sp,b〉 ← opt_to_res ? (find_symbol ? ? ge (prog_main ?? p));
    657   do u ← opt_to_res ? (match eq_region_dec sp Code with [ inl _ ⇒ Some ? it | inr _ ⇒ None ? ]);
     656  do b ← opt_to_res ? (find_symbol ? ? ge (prog_main ?? p));
    658657  do f ← opt_to_res ? (find_funct_ptr ? ? ge b);
    659658  OK ? 〈ge,Callstate f (nil ?) Kstop m0〉.
Note: See TracChangeset for help on using the changeset viewer.