Ignore:
Timestamp:
May 24, 2012, 11:39:27 AM (6 years ago)
Author:
campbell
Message:

Abstraction of the memory contents in the memory models is no longer
necessary.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Cminor/semantics.ma

    r1986 r1988  
    300300        | Kblock k' ⇒ λkInv. return 〈E0, State f St_skip en fInv ? m sp k' ? st〉
    301301          (* cminor allows functions without an explicit return statement *)
    302         | Kend ⇒ λkInv. return 〈E0, Returnstate (None ?) (free ? m sp) st〉
     302        | Kend ⇒ λkInv. return 〈E0, Returnstate (None ?) (free m sp) st〉
    303303        ] kInv
    304304    | St_assign _ id e ⇒ λInv.
     
    345345    | St_return eo ⇒
    346346        match eo return λeo. stmt_inv f en (St_return eo) → ? with
    347         [ None ⇒ λInv. return 〈E0, Returnstate (None ?) (free ? m sp) st〉
     347        [ None ⇒ λInv. return 〈E0, Returnstate (None ?) (free m sp) st〉
    348348        | Some e ⇒
    349349            match e return λe. stmt_inv f en (St_return (Some ? e)) → ? with [ mk_DPair ty e ⇒ λInv.
    350350              ! 〈tr,v〉 ← eval_expr ge ? e en ? sp m;
    351               return 〈tr, Returnstate (Some ? v) (free ? m sp) st〉
     351              return 〈tr, Returnstate (Some ? v) (free m sp) st〉
    352352            ]
    353353        ]
     
    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) Any 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.