Changeset 619 for Deliverables/D2.2/8051/src/LTL
- Timestamp:
- Mar 2, 2011, 3:27:41 PM (10 years ago)
- Location:
- Deliverables/D2.2/8051/src/LTL
- Files:
-
- 2 edited
Legend:
- Unmodified
- Added
- Removed
-
Deliverables/D2.2/8051/src/LTL/LTLInterpret.ml
r486 r619 45 45 renv : hdw_reg_env ; 46 46 mem : memory ; 47 trace : AST.trace}47 trace : CostLabel.t list } 48 48 49 49 … … 371 371 (string_of_reg I8051.dph) (string_of_reg I8051.dpl) 372 372 373 let rec iter_small_step lbls_offs st = 373 let 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 378 let rec iter_small_step print_result lbls_offs st = 374 379 (* 375 380 print_state lbls_offs st ; … … 377 382 match fetch_stmt lbls_offs st with 378 383 | 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.trace384 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 384 389 | stmt -> 385 390 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' 387 392 388 393 … … 446 451 - Initialize the carry flag to 0. *) 447 452 448 let interpret p = match p.LTL.main with449 | None -> []453 let interpret print_result p = match p.LTL.main with 454 | None -> (IntValue.Int8.zero, []) 450 455 | Some main -> 451 456 let lbls_offs = labels_offsets p in … … 457 462 let st = init_main_call lbls_offs st main in 458 463 let st = change_carry st Val.zero in 459 iter_small_step lbls_offs st464 iter_small_step print_result lbls_offs st -
Deliverables/D2.2/8051/src/LTL/LTLInterpret.mli
r486 r619 3 3 return the trace of cost labels encountered. *) 4 4 5 val interpret: LTL.program -> AST.trace5 val interpret: bool -> LTL.program -> AST.trace
Note: See TracChangeset
for help on using the changeset viewer.