Changeset 1986 for src/Clight/Csem.ma


Ignore:
Timestamp:
May 24, 2012, 9:35:08 AM (8 years ago)
Author:
campbell
Message:

Get rid of unused abstraction of Globalenvs.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/Csem.ma

    r1914 r1986  
    468468  and function pointers to their definitions.  (See module [Globalenvs].) *)
    469469
    470 definition genv ≝ (genv_t Genv) clight_fundef.
     470definition genv ≝ genv_t clight_fundef.
    471471
    472472(* * The local environment maps local variables to block references.
     
    662662  | eval_Evar_global: ∀id,l,ty.
    663663      (* XXX e!id *) lookup ?? e id = None ? →
    664       find_symbol ?? ge id = Some ? l →
     664      find_symbol ge id = Some ? l →
    665665      eval_lvalue ge e m (Expr (Evar id) ty) l zero_offset E0
    666666  | eval_Ederef: ∀a,ty,r,l,p,ofs,tr.
     
    10361036      eval_expr ge e m a vf tr1 →
    10371037      eval_exprlist ge e m al vargs tr2 →
    1038       find_funct ?? ge vf = Some ? fd →
     1038      find_funct ge vf = Some ? fd →
    10391039      type_of_fundef fd = fun_typeof a →
    10401040      step ge (State f (Scall (None ?) a al) k e m)
     
    10451045      eval_expr ge e m a vf tr2 →
    10461046      eval_exprlist ge e m al vargs tr3 →
    1047       find_funct ?? ge vf = Some ? fd →
     1047      find_funct ge vf = Some ? fd →
    10481048      type_of_fundef fd = fun_typeof a →
    10491049      step ge (State f (Scall (Some ? lhs) a al) k e m)
     
    12131213inductive initial_state (p: clight_program): state -> Prop :=
    12141214  | initial_state_intro: ∀b,f,ge,m0.
    1215       globalenv Genv ?? (fst ??) p = ge →
    1216       init_mem Genv ?? (fst ??) p = OK ? m0 →
    1217       find_symbol ?? ge (prog_main ?? p) = Some ? b →
    1218       find_funct_ptr ?? ge b = Some ? f →
     1215      globalenv (fst ??) p = ge →
     1216      init_mem (fst ??) p = OK ? m0 →
     1217      find_symbol ge (prog_main ?? p) = Some ? b →
     1218      find_funct_ptr ge b = Some ? f →
    12191219      initial_state p (Callstate f (nil ?) Kstop m0).
    12201220
     
    12311231
    12321232definition exec_program : clight_program → program_behavior → Prop ≝ λp,beh.
    1233   ∀ge. globalenv ??? (fst ??) p = ge →
     1233  ∀ge. globalenv (fst ??) p = ge →
    12341234  program_behaves (mk_transrel ?? step) (initial_state p) final_state ge beh.
    12351235 
Note: See TracChangeset for help on using the changeset viewer.