Ignore:
Timestamp:
Aug 30, 2011, 6:55:12 PM (8 years ago)
Author:
campbell
Message:

Merge trunk into branch.

Location:
Deliverables/D3.3/id-lookup-branch
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.3/id-lookup-branch

  • Deliverables/D3.3/id-lookup-branch/RTLabs/semantics.ma

    r961 r1153  
    168168    [ Internal fn ⇒
    169169        ! locals ← params_store (f_params fn) params (init_locals (f_locals fn));
     170        (* CSC: XXX alignment call (concrete_stacksize in OCaml) is missing
     171           here *)
    170172        let 〈m', sp〉 ≝ alloc m 0 (f_stacksize fn) Any in
    171173        ret ? 〈E0, State (mk_frame fn locals (f_entry fn) sp dst) fs m'〉
     
    207209definition make_initial_state : RTLabs_program → res (genv × state) ≝
    208210λp.
    209   do ge ← globalenv Genv ?? p;
    210   do m ← init_mem Genv ?? p;
     211  do ge ← globalenv Genv ?? (λx.[Init_space x]) p;
     212  do m ← init_mem Genv ?? (λx.[Init_space x]) p;
    211213  let main ≝ prog_main ?? p in
    212214  do b ← opt_to_res ? [MSG MissingSymbol; CTX ? main] (find_symbol ? ? ge main);
Note: See TracChangeset for help on using the changeset viewer.