Ignore:
Timestamp:
Apr 4, 2011, 5:18:15 PM (9 years ago)
Author:
ayache
Message:

New memory model and bug fixes in 8051 branch. Added primitive operations in interpreters from Clight to LIN.

File:
1 edited

Legend:

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

    r640 r740  
    2929    | None -> (false, filename)
    3030    | Some filename' -> (true, filename') in
    31   let save = Languages.save exact_output output_filename in
     31  let save ?(suffix="") ast =
     32    Languages.save exact_output output_filename suffix ast
     33  in
    3234  let target_asts =
    3335    (** If debugging is enabled, the compilation function returns all
     
    3739  in
    3840  let final_ast, intermediate_asts = Misc.ListExt.cut_last target_asts in
    39     save final_ast;
    40     (if Options.annotation_requested () then
    41        let (annotated_input_ast, cost_id, cost_incr) =
    42          Languages.annotate input_ast final_ast in
    43        save annotated_input_ast;
    44        Languages.save_cost output_filename cost_id cost_incr);
    45     (if Options.is_debug_enabled () then
    46       List.iter save intermediate_asts);
    47     if Options.interpretation_requested () || Options.is_debug_enabled () then
    48       begin
    49         let asts = input_ast :: target_asts in
    50         let print_result = Options.is_print_result_enabled () in
    51         let label_traces = List.map (Languages.interpret print_result) asts in
    52         Printf.eprintf "Checking execution traces...%!";
    53         Checker.same_traces (List.combine asts label_traces);
    54         Printf.eprintf "OK.\n%!";
    55       end
     41  save final_ast;
     42  if Options.annotation_requested () then
     43    begin
     44      let (annotated_input_ast, cost_id, cost_incr) =
     45        Languages.annotate input_ast final_ast in (
     46          save ~suffix:"-annotated" annotated_input_ast;
     47          Languages.save_cost output_filename cost_id cost_incr);
     48    end;
     49                                             
     50  if Options.is_debug_enabled () then
     51    List.iter save intermediate_asts;
     52
     53  if Options.interpretation_requested () || Options.is_debug_enabled () then
     54    begin
     55      let asts = input_ast :: target_asts in
     56      let label_traces = List.map (Languages.interpret false) asts in
     57      Printf.eprintf "Checking execution traces...%!";
     58      Checker.same_traces (List.combine asts label_traces);
     59      Printf.eprintf "OK.\n%!";
     60    end
    5661
    5762let _ =
Note: See TracChangeset for help on using the changeset viewer.