Ignore:
Timestamp:
Oct 7, 2011, 5:47:39 PM (9 years ago)
Author:
tranquil
Message:
  • bug in ClightUtilities?.find_max_depth_lbld fixed
  • single-entry loop detection completed
  • work on Clight completed
File:
1 edited

Legend:

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

    r818 r1328  
    5454    List.iter save intermediate_asts;
    5555
    56   if Options.interpretation_requested () || Options.is_debug_enabled () then
     56  if Options.interpretation_requested () || Options.is_debug_enabled () ||
     57               Options.trace_requested () then
    5758    begin
    5859      let asts = target_asts in
     
    6061      let label_traces = List.map (Languages.interpret debug) asts in
    6162      Printf.eprintf "Checking execution traces...%!";
     63                        if Options.trace_requested () then
     64                                let print_l l =
     65                                        Printf.printf "%s, " (CostLabel.string_of_cost_label
     66                                                               ~pretty:true l) in
     67                          let print_ls ls = List.iter print_l (List.rev ls) in
     68                                let print_trace (v, ls) =
     69                                        Printf.printf "%s | " (Big_int.string_of_big_int v);
     70                                        print_ls ls;
     71                                        Printf.printf "\n" in
     72                                List.iter print_trace label_traces
     73                        else ();
    6274      Checker.same_traces (List.combine asts label_traces);
    6375      Printf.eprintf "OK.\n%!";
Note: See TracChangeset for help on using the changeset viewer.