Ignore:
Timestamp:
Dec 6, 2011, 5:04:13 PM (9 years ago)
Author:
tranquil
Message:
  • turned to argument-less return statements for RTLabs and RTL (there was a hidden invariant, for which the arguments of return statements where equal to the f_result field of the function definition: they were useless and an optimization was breaking the compilation)
  • corrected a bug in liveness analysis I had introduced
File:
1 edited

Legend:

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

    r1585 r1589  
    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 =   Printf.printf "forgetting\n";
    50 { st with inds = CostLabel.forget_const_ind st.inds }
     49let forget_ind st = { st with inds = CostLabel.forget_const_ind st.inds }
    5150let enter_loop st = CostLabel.enter_loop st.inds
    5251let continue_loop st = CostLabel.continue_loop st.inds
     
    102101  Val.change_address_offset ptr (Labels_Offsets.find1 def.LTL.f_entry lbls_offs)
    103102
    104 let init_fun_call name lbls_offs st ptr def =
     103let init_fun_call lbls_offs st ptr def =
    105104  let pc = entry_pc lbls_offs ptr def in
    106105  let st = new_ind st in
    107   Printf.printf "calling %s\n" name;
    108106  change_pc st pc
    109107
     
    149147
    150148let label_of_pointer lbls_offs ptr =
    151 (*
    152   Printf.printf "Retrieving label of %s\n%!" (Val.to_string ptr) ;
    153 *)
    154149  let off = Val.offset_of_address ptr in
    155150  Labels_Offsets.find2 off lbls_offs
     
    211206  change_pc st next_pc
    212207
    213 let interpret_call name lbls_offs st ptr ra =
     208let interpret_call lbls_offs st ptr ra =
    214209  match Mem.find_fun_def st.mem ptr with
    215210    | LTL.F_int def ->
    216211      let st = save_ra lbls_offs st ra in
    217       init_fun_call name lbls_offs st ptr def
     212      init_fun_call lbls_offs st ptr def
    218213    | LTL.F_ext def ->
    219214      let next_pc =
     
    222217
    223218let interpret_return lbls_offs st =
    224   Printf.printf "returning\n";
    225219  let st = forget_ind st in
    226220  let (st, pc) = return_pc st in
     
    328322
    329323    | LTL.St_call_id (f, lbl) ->
    330       interpret_call f lbls_offs st (Mem.find_global st.mem f) lbl
     324      interpret_call lbls_offs st (Mem.find_global st.mem f) lbl
    331325
    332326    | LTL.St_call_ptr lbl ->
    333       interpret_call (Val.string_of_address (dptr st)) lbls_offs st (dptr st) lbl
     327      interpret_call lbls_offs st (dptr st) lbl
    334328
    335329    | LTL.St_condacc (lbl_true, lbl_false) ->
     
    362356    (res, cost_labels) in
    363357  if debug then print_state lbls_offs st ;
    364   Printf.printf "%s\n" (Val.string_of_address st.pc);
    365358  match fetch_stmt lbls_offs st with
    366359    | LTL.St_return when Val.eq_address (snd (return_pc st)) st.exit ->
     
    411404  match Mem.find_fun_def st.mem ptr with
    412405    | LTL.F_int def ->
    413       init_fun_call main lbls_offs st ptr def
     406      init_fun_call lbls_offs st ptr def
    414407    | _ -> error ("Cannot execute the main (\"" ^ main ^ "\"): it is external.")
    415408
Note: See TracChangeset for help on using the changeset viewer.