Changeset 761 for src/RTLabs


Ignore:
Timestamp:
Apr 19, 2011, 12:22:32 PM (9 years ago)
Author:
campbell
Message:

Enforce the use of declared identifiers/registers in Cminor/RTLabs.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/RTLabs-sem.ma

    r751 r761  
    4848definition build_state ≝ λf.λfs.λm.λn. State (adv n f) fs m.
    4949
     50definition init_locals : list register → register_env val ≝
     51foldr ?? (λid,en. add RegisterTag val en id Vundef) (empty_map ??).
     52
    5053definition reg_store ≝
    5154λreg,v,locals.
    52   OK ? (add RegisterTag val locals reg v)
    53 .
     55  update RegisterTag val locals reg v.
    5456
    5557let rec params_store (rs:list register) (vs:list val) (locals : register_env val) : res (register_env val) ≝
     
    5759[ nil ⇒ match vs with [ nil ⇒ OK ? locals | _ ⇒ Error ? ]
    5860| cons r rst ⇒ match vs with [ nil ⇒ Error ? | cons v vst ⇒
    59   do locals' ← reg_store r v locals;
     61  let locals' ≝ add RegisterTag val locals r v in
    6062  params_store rst vst locals'
    6163] ].
     
    182184    match fd with
    183185    [ Internal fn ⇒
    184         ! locals ← params_store (f_params fn) params (empty_map RegisterTag ?);
     186        ! locals ← params_store (f_params fn) params (init_locals (f_locals fn));
    185187        let 〈m', sp〉 ≝ alloc m 0 (f_stacksize fn) Any in
    186188        ret ? 〈E0, State (mk_frame fn locals (f_entry fn) sp dst) fs m'〉
Note: See TracChangeset for help on using the changeset viewer.