Changeset 2968 for src/joint


Ignore:
Timestamp:
Mar 26, 2013, 7:07:51 PM (7 years ago)
Author:
sacerdot
Message:

The initial status memory was not really initialized. Now it is.

Location:
src/joint
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/joint/Traces.ma

    r2967 r2968  
    2323
    2424definition make_initial_state :
    25  ∀pars: prog_params.state_pc pars
     25 ∀pars: prog_params.res (state_pc pars)
    2626λpars.let p ≝ prog pars in
    2727  let ge ≝ ev_genv pars in
    2828  (* this is going to change shortly: globals will not reside in globalenv anymore *)
    29   let m0 ≝ \snd (globalenv_allocmem … (λx.x) p) in
     29  ! m0 ← init_mem … (λx.x) p ;
    3030  let 〈m,spb〉 as H ≝ alloc … m0 0 external_ram_size in
    3131  let globals_size ≝ globals_stacksize … p in
     
    4545    (* mem ≝ *)m
    4646    (* stack_usage ≝ *)globals_size in
     47  return
    4748  mk_state_pc ?
    4849    (* state_no_pc ≝ *)(set_sp … spp st)
  • src/joint/joint_fullexec.ma

    r2952 r2968  
    1616    (λpr.joint_make_global (mk_prog_params G (\fst pr) (\snd pr)))
    1717    (λp_stacks.
    18       return make_initial_state (mk_prog_params G (\fst p_stacks) (\snd p_stacks))).
     18      make_initial_state (mk_prog_params G (\fst p_stacks) (\snd p_stacks))).
    1919
    2020definition joint_preclassified_system : sem_params →
Note: See TracChangeset for help on using the changeset viewer.