Ignore:
Timestamp:
Feb 9, 2012, 1:22:28 PM (8 years ago)
Author:
campbell
Message:

Comment out unused tailcalls in Cminor and RTLabs.
(They would be a little tricky to deal with in RTLabs/Traces.ma, and we
don't currently generate them.)

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Cminor/semantics.ma

    r1655 r1680  
    320320        ! 〈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 ?;
    321321        return 〈tr ⧺ tr', Callstate fd vargs m (Scall dst f sp en ? fInv k ? st)〉
     322(*
    322323    | St_tailcall ef args ⇒ λInv.
    323324        ! 〈tr,vf〉 ← eval_expr ge ? ef en ? sp m;
     
    325326        ! 〈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 ?;
    326327        return 〈tr ⧺ tr', Callstate fd vargs (free m sp) st〉
    327        
     328*)       
    328329    | St_seq s1 s2 ⇒ λInv. return 〈E0, State f s1 en fInv ? m sp (Kseq s2 k) ? st〉
    329330    | St_ifthenelse _ _ e strue sfalse ⇒ λInv.
Note: See TracChangeset for help on using the changeset viewer.