Changeset 2722 for src/Clight/Csem.ma


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/Clight/Csem.ma

    r2677 r2722  
    933933      ∀m: mem.  state
    934934  | Callstate:
    935       ∀fb: val. (* function pointer; used by stack instrumentation, but not the semantics *)
     935      ∀id: ident. (* function name; used by stack instrumentation, but not the semantics *)
    936936      ∀fd: clight_fundef.
    937937      ∀args: list val.
     
    10251025           (tr1⧺tr2) (State f Sskip k e m')
    10261026
    1027   | step_call_none:   ∀f,a,al,k,e,m,vf,vargs,fd,tr1,tr2.
     1027  | step_call_none:   ∀f,a,al,k,e,m,vf,vargs,fd,id,tr1,tr2.
    10281028      eval_expr ge e m a vf tr1 →
    10291029      eval_exprlist ge e m al vargs tr2 →
    1030       find_funct … ge vf = Some ? fd
     1030      find_funct_id … ge vf = Some ? 〈fd,id〉
    10311031      type_of_fundef fd = fun_typeof a →
    10321032      step ge (State f (Scall (None ?) a al) k e m)
    1033            (tr1⧺tr2) (Callstate vf fd vargs (Kcall (None ?) f e k) m)
    1034 
    1035   | step_call_some:   ∀f,lhs,a,al,k,e,m,loc,ofs,vf,vargs,fd,tr1,tr2,tr3.
     1033           (tr1⧺tr2) (Callstate id fd vargs (Kcall (None ?) f e k) m)
     1034
     1035  | step_call_some:   ∀f,lhs,a,al,k,e,m,loc,ofs,vf,vargs,fd,id,tr1,tr2,tr3.
    10361036      eval_lvalue ge e m lhs loc ofs tr1 →
    10371037      eval_expr ge e m a vf tr2 →
    10381038      eval_exprlist ge e m al vargs tr3 →
    1039       find_funct … ge vf = Some ? fd
     1039      find_funct_id … ge vf = Some ? 〈fd,id〉
    10401040      type_of_fundef fd = fun_typeof a →
    10411041      step ge (State f (Scall (Some ? lhs) a al) k e m)
    1042            (tr1⧺tr2⧺tr3) (Callstate vf fd vargs (Kcall (Some ? 〈〈loc, ofs〉, typeof lhs〉) f e k) m)
     1042           (tr1⧺tr2⧺tr3) (Callstate id fd vargs (Kcall (Some ? 〈〈loc, ofs〉, typeof lhs〉) f e k) m)
    10431043
    10441044  | step_seq:  ∀f,s1,s2,k,e,m.
     
    11661166           E0 (State f s' k' e m)
    11671167
    1168   | step_internal_function: ∀vf,f,vargs,k,m,e,m1,m2.
     1168  | step_internal_function: ∀id,f,vargs,k,m,e,m1,m2.
    11691169      alloc_variables empty_env m ((fn_params f) @ (fn_vars f)) e m1 →
    11701170      bind_parameters e m1 (fn_params f) vargs m2 →
    1171       step ge (Callstate vf (CL_Internal f) vargs k m)
     1171      step ge (Callstate id (CL_Internal f) vargs k m)
    11721172           E0 (State f (fn_body f) k e m2)
    11731173
    1174   | step_external_function: ∀vf,id,targs,tres,vargs,k,m,vres,t.
     1174  | step_external_function: ∀fid,id,targs,tres,vargs,k,m,vres,t.
    11751175      event_match (external_function id targs tres) vargs t vres →
    1176       step ge (Callstate vf (CL_External id targs tres) vargs k m)
     1176      step ge (Callstate fid (CL_External id targs tres) vargs k m)
    11771177            t (Returnstate vres k m)
    11781178
     
    12111211      find_symbol … ge (prog_main ?? p) = Some ? b →
    12121212      find_funct_ptr … ge b = Some ? f →
    1213       initial_state p (Callstate (Vptr (mk_pointer b zero_offset)) f (nil ?) Kstop m0).
     1213      initial_state p (Callstate (prog_main ?? p) f (nil ?) Kstop m0).
    12141214
    12151215(* * A final state is a [Returnstate] with an empty continuation. *)
Note: See TracChangeset for help on using the changeset viewer.