Ignore:
Timestamp:
Mar 2, 2011, 3:27:41 PM (9 years ago)
Author:
ayache
Message:

Update of D2.2 from Paris.

File:
1 edited

Legend:

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

    r486 r619  
    4545      renv   : hdw_reg_env ;
    4646      mem    : memory ;
    47       trace  : AST.trace }
     47      trace  : CostLabel.t list }
    4848
    4949
     
    371371    (string_of_reg I8051.dph) (string_of_reg I8051.dpl)
    372372
    373 let rec iter_small_step lbls_offs st =
     373let compute_result st =
     374  let v = get_reg I8051.dpl st in
     375  if Val.is_int v then IntValue.Int8.cast (Val.to_int_repr v)
     376  else IntValue.Int8.zero
     377
     378let rec iter_small_step print_result lbls_offs st =
    374379(*
    375380    print_state lbls_offs st ;
     
    377382  match fetch_stmt lbls_offs st with
    378383    | LTL.St_return when Val.eq (return_pc st) Val.zero ->
    379 (*
    380       print_state lbls_offs st ;
    381       print_result st ;
    382 *)
    383       List.rev st.trace
     384      let (res, cost_labels) as trace =
     385        (compute_result st, List.rev st.trace) in
     386      if print_result then
     387        Printf.printf "LTL: %s\n%!" (IntValue.Int8.to_string res) ;
     388      trace
    384389    | stmt ->
    385390      let st' = interpret_stmt lbls_offs st stmt in
    386       iter_small_step lbls_offs st'
     391      iter_small_step print_result lbls_offs st'
    387392
    388393
     
    446451   - Initialize the carry flag to 0. *)
    447452
    448 let interpret p = match p.LTL.main with
    449   | None -> []
     453let interpret print_result p = match p.LTL.main with
     454  | None -> (IntValue.Int8.zero, [])
    450455  | Some main ->
    451456    let lbls_offs = labels_offsets p in
     
    457462    let st = init_main_call lbls_offs st main in
    458463    let st = change_carry st Val.zero in
    459     iter_small_step lbls_offs st
     464    iter_small_step print_result lbls_offs st
Note: See TracChangeset for help on using the changeset viewer.