Changeset 1986 for src/Clight/Cexec.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/Cexec.ma

    r1874 r1986  
    242242  [ Evar id ⇒
    243243      match (lookup ?? en id) with
    244       [ None ⇒ do l ← opt_to_res ? [MSG UnknownIdentifier; CTX ? id] (find_symbol ? ? ge id); OK ? 〈〈l,zero_offset〉,E0〉 (* global *)
     244      [ None ⇒ do l ← opt_to_res ? [MSG UnknownIdentifier; CTX ? id] (find_symbol ge id); OK ? 〈〈l,zero_offset〉,E0〉 (* global *)
    245245      | Some loc ⇒ OK ? 〈〈loc,zero_offset〉,E0〉 (* local *)
    246246      ]
     
    357357    ! 〈vf,tr2〉 ← exec_expr ge e m a : IO ???;
    358358    ! 〈vargs,tr3〉 ← exec_exprlist ge e m al : IO ???;
    359     ! fd ← opt_to_io … (msg BadFunctionValue) (find_funct ? ? ge vf);
     359    ! fd ← opt_to_io … (msg BadFunctionValue) (find_funct ge vf);
    360360    ! p ← err_to_io … (assert_type_eq (type_of_fundef fd) (fun_typeof a));
    361361(* requires associativity of IOMonad, so rearrange it below
     
    504504
    505505definition make_global : clight_program → genv ≝
    506 λp. globalenv Genv ?? (fst ??) p.
     506λp. globalenv (fst ??) p.
    507507
    508508let rec make_initial_state (p:clight_program) : res state ≝
    509509  let ge ≝ make_global p in
    510   do m0 ← init_mem Genv ?? (fst ??) p;
    511   do b ← opt_to_res ? (msg MainMissing) (find_symbol ? ? ge (prog_main ?? p));
    512   do f ← opt_to_res ? (msg MainMissing) (find_funct_ptr ? ? ge b);
     510  do m0 ← init_mem (fst ??) p;
     511  do b ← opt_to_res ? (msg MainMissing) (find_symbol ge (prog_main ?? p));
     512  do f ← opt_to_res ? (msg MainMissing) (find_funct_ptr ge b);
    513513  OK ? (Callstate f (nil ?) Kstop m0).
    514514
Note: See TracChangeset for help on using the changeset viewer.