Ignore:
Timestamp:
Jul 12, 2012, 1:28:28 PM (7 years ago)
Author:
campbell
Message:

Remove memory spaces other than XData and Code; simplify pointers as a
result.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Cminor/semantics.ma

    r1993 r2176  
    106106    do r ← opt_to_res … (msg FailedOp) (eval_binop ??? op v1 v2);
    107107    OK ? 〈tr1 ⧺ tr2, r〉
    108 | Mem ty rg e ⇒ λEnv.
     108| Mem ty e ⇒ λEnv.
    109109    do 〈tr,v〉 ← eval_expr ge ? e en ? sp m;
    110110    do r ← opt_to_res … (msg FailedLoad) (loadv ty m v);
     
    306306        let en' ≝ update_present ?? en id ? v in
    307307        return 〈tr, State f St_skip en' ? ? m sp k ? st〉
    308     | St_store ty _ edst e ⇒ λInv.
     308    | St_store ty edst e ⇒ λInv.
    309309        ! 〈tr,vdst〉 ← eval_expr ge ? edst en ? sp m;
    310310        ! 〈tr',v〉 ← eval_expr ge ? e en ? sp m;
     
    363363    match fd with
    364364    [ Internal f ⇒ err_to_io ?? (trace × state) (
    365         let 〈m',sp〉 ≝ alloc m 0 (f_stacksize f) Any in
     365        let 〈m',sp〉 ≝ alloc m 0 (f_stacksize f) XData in
    366366        ! en ← bind_params args (f_params f);
    367367        return 〈E0, State f (f_body f) (init_locals en (f_vars f)) ? ? m' sp Kend ? st〉)
Note: See TracChangeset for help on using the changeset viewer.