Ignore:
Timestamp:
Nov 15, 2011, 5:11:19 PM (9 years ago)
Author:
tranquil
Message:
  • added an option to not use ternary expressions in costs, to accomodate frama-c explosion of such expressions
  • corrected some typos in comments
  • added a check for well behaved for loops in loop unrolling, but intelligent unrolling is not done yet
  • TODO: peeling and unrolling can contradict preciseness (with difference between introduced branches around 2 cycles). I guess it can be corrected easily
File:
1 edited

Legend:

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

    r1433 r1507  
    4646    begin
    4747      let (annotated_input_ast, cost_id, cost_incr) =
    48         Languages.annotate input_ast final_ast in (
     48        let cost_tern = Options.is_cost_ternary_enabled () in
     49        Languages.annotate cost_tern input_ast final_ast in (
    4950          save ~suffix:"-annotated" annotated_input_ast;
    5051          Languages.save_cost output_filename cost_id cost_incr);
     
    6162      let label_traces = List.map (Languages.interpret debug) asts in
    6263      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 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 ();
     64      if Options.trace_requested () then
     65        let print_l l =
     66          Printf.printf "%s, " (CostLabel.string_of_cost_label
     67                                  ~pretty:true l) in
     68        let print_ls ls = List.iter print_l ls in
     69        let print_trace (v, ls) =
     70          Printf.printf "%s | " (Big_int.string_of_big_int v);
     71          print_ls ls;
     72          Printf.printf "\n" in
     73        List.iter print_trace label_traces
     74      else ();
    7475      Checker.same_traces (List.combine asts label_traces);
    7576      Printf.eprintf "OK.\n%!";
Note: See TracChangeset for help on using the changeset viewer.