Ignore:
Timestamp:
Nov 23, 2011, 1:55:12 PM (9 years ago)
Author:
tranquil
Message:

branch up to date

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D2.2/8051-indexed-labels-branch/src/LTL/LTLInterpret.ml

    r1357 r1539  
    3131      renv   : hdw_reg_env ;
    3232      mem    : memory ;
    33                         inds   : CostLabel.const_indexing list ;
     33      inds   : CostLabel.const_indexing list ;
    3434      trace  : CostLabel.t list }
    3535
     
    5858    renv   = I8051.RegisterMap.empty ;
    5959    mem    = Mem.empty ;
    60                 inds   = [] ;
     60    inds   = [] ;
    6161    trace  = [] }
    6262
     
    102102let init_fun_call lbls_offs st ptr def =
    103103  let pc = entry_pc lbls_offs ptr def in
    104         let st = new_ind st in
     104  let st = new_ind st in
    105105  change_pc st pc
    106106
     
    204204  change_pc st next_pc
    205205
    206 let interpret_call lbls_offs st f ra =
    207   let ptr = Mem.find_global st.mem f in
     206let interpret_call lbls_offs st ptr ra =
    208207  match Mem.find_fun_def st.mem ptr with
    209208    | LTL.F_int def ->
     
    216215
    217216let interpret_return lbls_offs st =
    218         let st = forget_ind st in
     217  let st = forget_ind st in
    219218  let (st, pc) = return_pc st in
    220219  change_pc st pc
     
    237236
    238237    | LTL.St_cost (cost_lbl, lbl) ->
    239                         let cost_lbl = ev_label st cost_lbl in
     238      let cost_lbl = ev_label st cost_lbl in
    240239      let st = add_trace st cost_lbl in
    241240      next_pc st lbl
    242241
    243242    | LTL.St_ind_0 (i, lbl) ->
    244             enter_loop st i;
    245             next_pc st lbl
     243      enter_loop st i;
     244      next_pc st lbl
    246245
    247246    | LTL.St_ind_inc (i, lbl) ->
     
    249248      next_pc st lbl
    250249
    251                 | LTL.St_int (r, i, lbl) ->
     250    | LTL.St_int (r, i, lbl) ->
    252251      let st = add_reg r (Val.of_int i) st in
    253252      next_pc st lbl
     
    321320
    322321    | LTL.St_call_id (f, lbl) ->
    323       interpret_call lbls_offs st f lbl
     322      interpret_call lbls_offs st (Mem.find_global st.mem f) lbl
     323
     324    | LTL.St_call_ptr lbl ->
     325      interpret_call lbls_offs st (dptr st) lbl
    324326
    325327    | LTL.St_condacc (lbl_true, lbl_false) ->
Note: See TracChangeset for help on using the changeset viewer.