Ignore:
Timestamp:
Nov 23, 2011, 5:43:24 PM (9 years ago)
Author:
tranquil
Message:

merge of indexed labels branch

File:
1 edited

Legend:

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

    r1488 r1542  
    3131      renv   : hdw_reg_env ;
    3232      mem    : memory ;
     33      inds   : CostLabel.const_indexing list ;
    3334      trace  : CostLabel.t list }
    3435
     
    4445let change_trace st trace = { st with trace = trace }
    4546let add_trace st cost_lbl = change_trace st (cost_lbl :: st.trace)
     47let ev_label st = CostLabel.ev_indexing (CostLabel.curr_const_ind st.inds)
     48let new_ind st = { st with inds = CostLabel.new_const_ind st.inds }
     49let forget_ind st = { st with inds = CostLabel.forget_const_ind st.inds }
     50let enter_loop st = CostLabel.enter_loop st.inds
     51let continue_loop st = CostLabel.continue_loop st.inds
    4652
    4753let empty_state =
     
    5258    renv   = I8051.RegisterMap.empty ;
    5359    mem    = Mem.empty ;
     60    inds   = [] ;
    5461    trace  = [] }
    5562
     
    95102let init_fun_call lbls_offs st ptr def =
    96103  let pc = entry_pc lbls_offs ptr def in
     104  let st = new_ind st in
    97105  change_pc st pc
    98106
     
    207215
    208216let interpret_return lbls_offs st =
     217  let st = forget_ind st in
    209218  let (st, pc) = return_pc st in
    210219  change_pc st pc
     
    227236
    228237    | LTL.St_cost (cost_lbl, lbl) ->
     238      let cost_lbl = ev_label st cost_lbl in
    229239      let st = add_trace st cost_lbl in
     240      next_pc st lbl
     241
     242    | LTL.St_ind_0 (i, lbl) ->
     243      enter_loop st i;
     244      next_pc st lbl
     245
     246    | LTL.St_ind_inc (i, lbl) ->
     247      continue_loop st i;
    230248      next_pc st lbl
    231249
Note: See TracChangeset for help on using the changeset viewer.