Ignore:
Timestamp:
Dec 2, 2011, 7:49:19 PM (8 years ago)
Author:
tranquil
Message:

fighting with a bug of the translation from RTL to ERTL

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D2.2/8051/src/LTL/LTLInterpret.ml

    r1572 r1585  
    4747let ev_label st = CostLabel.ev_indexing (CostLabel.curr_const_ind st.inds)
    4848let new_ind st = { st with inds = CostLabel.new_const_ind st.inds }
    49 let forget_ind st = { st with inds = CostLabel.forget_const_ind st.inds }
     49let forget_ind st =   Printf.printf "forgetting\n";
     50{ st with inds = CostLabel.forget_const_ind st.inds }
    5051let enter_loop st = CostLabel.enter_loop st.inds
    5152let continue_loop st = CostLabel.continue_loop st.inds
     
    101102  Val.change_address_offset ptr (Labels_Offsets.find1 def.LTL.f_entry lbls_offs)
    102103
    103 let init_fun_call lbls_offs st ptr def =
     104let init_fun_call name lbls_offs st ptr def =
    104105  let pc = entry_pc lbls_offs ptr def in
    105106  let st = new_ind st in
     107  Printf.printf "calling %s\n" name;
    106108  change_pc st pc
    107109
     
    209211  change_pc st next_pc
    210212
    211 let interpret_call lbls_offs st ptr ra =
     213let interpret_call name lbls_offs st ptr ra =
    212214  match Mem.find_fun_def st.mem ptr with
    213215    | LTL.F_int def ->
    214216      let st = save_ra lbls_offs st ra in
    215       init_fun_call lbls_offs st ptr def
     217      init_fun_call name lbls_offs st ptr def
    216218    | LTL.F_ext def ->
    217219      let next_pc =
     
    220222
    221223let interpret_return lbls_offs st =
     224  Printf.printf "returning\n";
    222225  let st = forget_ind st in
    223226  let (st, pc) = return_pc st in
     
    325328
    326329    | LTL.St_call_id (f, lbl) ->
    327       interpret_call lbls_offs st (Mem.find_global st.mem f) lbl
     330      interpret_call f lbls_offs st (Mem.find_global st.mem f) lbl
    328331
    329332    | LTL.St_call_ptr lbl ->
    330       interpret_call lbls_offs st (dptr st) lbl
     333      interpret_call (Val.string_of_address (dptr st)) lbls_offs st (dptr st) lbl
    331334
    332335    | LTL.St_condacc (lbl_true, lbl_false) ->
     
    359362    (res, cost_labels) in
    360363  if debug then print_state lbls_offs st ;
     364  Printf.printf "%s\n" (Val.string_of_address st.pc);
    361365  match fetch_stmt lbls_offs st with
    362366    | LTL.St_return when Val.eq_address (snd (return_pc st)) st.exit ->
     
    407411  match Mem.find_fun_def st.mem ptr with
    408412    | LTL.F_int def ->
    409       init_fun_call lbls_offs st ptr def
     413      init_fun_call main lbls_offs st ptr def
    410414    | _ -> error ("Cannot execute the main (\"" ^ main ^ "\"): it is external.")
    411415
Note: See TracChangeset for help on using the changeset viewer.