Changeset 761 for src/Cminor


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

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

Location:
src/Cminor
Files:
1 added
1 edited

Legend:

Unmodified
Added
Removed
  • src/Cminor/semantics.ma

    r760 r761  
    134134].
    135135
     136definition init_locals : env → list ident → env ≝
     137foldr ?? (λid,en. add ?? en id Vundef).
     138
    136139definition eval_step : genv → state → IO io_out io_in (trace × state) ≝
    137140λge,st.
     
    149152    | St_assign id e ⇒
    150153        ! 〈tr,v〉 ← eval_expr ge e en sp m;
    151         ret ? 〈tr, State f St_skip (add ?? en id v) m sp k〉
     154        ! en' ← update ?? en id v;
     155        ret ? 〈tr, State f St_skip en' m sp k〉
    152156    | St_store chunk edst e ⇒
    153157        ! 〈tr,vdst〉 ← eval_expr ge edst en sp m;
     
    204208        let 〈m',sp〉 ≝ alloc m 0 (f_stacksize f) Any in
    205209        ! en ← bind_params args (f_params f);
    206         ret ? 〈E0, State f (f_body f) en m' sp k〉
     210        ret ? 〈E0, State f (f_body f) (init_locals en (f_vars f)) m' sp k〉
    207211    | External fn ⇒
    208212        ! evargs ← check_eventval_list args (sig_args (ef_sig fn));
     
    217221                [ None ⇒ match dst with [ None ⇒ OK ? en | Some _ ⇒ Error ? ]
    218222                | Some v ⇒ match dst with [ None ⇒ Error ?
    219                                           | Some id ⇒ OK ? (add ?? en id v) ]
     223                                          | Some id ⇒ update ?? en id v ]
    220224                ];
    221225        ret ? 〈E0, State f St_skip en' m sp k'〉
Note: See TracChangeset for help on using the changeset viewer.