Changeset 2722 for src/Cminor


Ignore:
Timestamp:
Feb 23, 2013, 5:05:03 PM (7 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/Cminor/Cminor_semantics.ma

    r2677 r2722  
    6969            state
    7070| Callstate:
    71     ∀   vf: val. (* fn pointer; only used for instrumentation, not the semantics *)
     71    ∀   id: ident. (* fn name; only used for instrumentation, not the semantics *)
    7272    ∀   fd: fundef internal_function.
    7373    ∀ args: list val.
     
    296296    | St_call dst ef args ⇒ λInv.
    297297        ! 〈tr,vf〉 ← eval_expr ge ? ef en ? sp m;
    298         ! fd ← opt_to_res … (msg BadFunctionValue) (find_funct … ge vf);
     298        ! 〈fd,id〉 ← opt_to_res … (msg BadFunctionValue) (find_funct_id … ge vf);
    299299        ! 〈tr',vargs〉 ← trace_map_inv … (λe. match e return λe.match e with [ mk_DPair _ _ ⇒ ? ] → ? with [ mk_DPair ty e ⇒ λp. eval_expr ge ? e en p sp m ]) args ?;
    300         return 〈tr ⧺ tr', Callstate vf fd vargs m (Scall dst f sp en ? fInv k ? st)〉
     300        return 〈tr ⧺ tr', Callstate id fd vargs m (Scall dst f sp en ? fInv k ? st)〉
    301301(*
    302302    | St_tailcall ef args ⇒ λInv.
     
    425425  do b ← opt_to_res ? (msg MainMissing) (find_symbol … ge (prog_main ?? p));
    426426  do f ← opt_to_res ? (msg MainMissing) (find_funct_ptr … ge b);
    427   OK ? (Callstate (Vptr (mk_pointer b zero_offset)) f (nil ?) m SStop).
     427  OK ? (Callstate (prog_main ?? p) f (nil ?) m SStop).
    428428
    429429definition Cminor_fullexec : fullexec io_out io_in ≝
     
    439439  do b ← opt_to_res ? (msg MainMissing) (find_symbol … ge (prog_main ?? p));
    440440  do f ← opt_to_res ? (msg MainMissing) (find_funct_ptr … ge b);
    441   OK ? (Callstate (Vptr (mk_pointer b zero_offset)) f (nil ?) m SStop).
     441  OK ? (Callstate (prog_main ?? p) f (nil ?) m SStop).
    442442
    443443definition Cminor_noinit_fullexec : fullexec io_out io_in ≝
Note: See TracChangeset for help on using the changeset viewer.