Changeset 2722 for src/Clight/Cexec.ma


Ignore:
Timestamp:
Feb 23, 2013, 5:05:03 PM (8 years ago)
Author:
campbell
Message:

It's easier to keep the real function identifier in front-end Callstates
than mucking around with the function pointer.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/Cexec.ma

    r2677 r2722  
    358358    ! 〈vf,tr2〉 ← exec_expr ge e m a : IO ???;
    359359    ! 〈vargs,tr3〉 ← exec_exprlist ge e m al : IO ???;
    360     ! fd ← opt_to_io … (msg BadFunctionValue) (find_funct … ge vf);
     360    ! 〈fd,id〉 ← opt_to_io … (msg BadFunctionValue) (find_funct_id … ge vf);
    361361    ! p ← err_to_io … (assert_type_eq (type_of_fundef fd) (fun_typeof a));
    362362(* requires associativity of IOMonad, so rearrange it below
     
    370370*)
    371371    match lhs with
    372          [ None ⇒ ret ? 〈tr2⧺tr3, Callstate vf fd vargs (Kcall (None ?) f e k) m〉
     372         [ None ⇒ ret ? 〈tr2⧺tr3, Callstate id fd vargs (Kcall (None ?) f e k) m〉
    373373         | Some lhs' ⇒
    374374           ! 〈locofs,tr1〉 ← exec_lvalue ge e m lhs' : IO ???;
    375            ret ? 〈tr1⧺tr2⧺tr3, Callstate vf fd vargs (Kcall (Some ? 〈locofs, typeof lhs'〉) f e k) m〉
     375           ret ? 〈tr1⧺tr2⧺tr3, Callstate id fd vargs (Kcall (Some ? 〈locofs, typeof lhs'〉) f e k) m〉
    376376         ]
    377377  | Ssequence s1 s2 ⇒ ret ? 〈E0, State f s1 (Kseq s2 k) e m〉
     
    521521  do b ← opt_to_res ? (msg MainMissing) (find_symbol … ge (prog_main ?? p));
    522522  do f ← opt_to_res ? (msg MainMissing) (find_funct_ptr … ge b);
    523   OK ? (Callstate (Vptr (mk_pointer b zero_offset)) f (nil ?) Kstop m0).
     523  OK ? (Callstate (prog_main ?? p) f (nil ?) Kstop m0).
    524524
    525525let rec is_final (s:state) : option int ≝
Note: See TracChangeset for help on using the changeset viewer.