Ignore:
Timestamp:
Oct 25, 2011, 4:11:11 PM (8 years ago)
Author:
ayache
Message:

Added D5.1: Frama-C plug-in and Lustre wrapper. D2.2 (8051) has been updated accordingly.

File:
1 edited

Legend:

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

    r818 r1462  
    2323*)
    2424let process filename =
    25   let _ = Printf.eprintf "Processing %s.\n%!" filename in
    26   let src_language    = Options.get_source_language () in
    27   let tgt_language    = Options.get_target_language () in
    28   let input_ast       = Languages.parse src_language filename in
    29   let input_ast       = Languages.add_runtime input_ast in
    30   let input_ast       = Languages.labelize input_ast in
     25  let _ = Printf.printf "Processing %s.\n%!" filename in
     26  let src_language = Options.get_source_language () in
     27  let tgt_language = Options.get_target_language () in
     28  let is_lustre_file = Options.is_lustre_file () in
     29  let remove_lustre_externals = Options.is_remove_lustre_externals () in
     30  let input_ast =
     31    Languages.parse ~is_lustre_file ~remove_lustre_externals
     32      src_language filename in
     33  let input_ast = Languages.add_runtime input_ast in
     34  let input_ast = Languages.labelize input_ast in
    3135  let (exact_output, output_filename) = match Options.get_output_files () with
    3236    | None -> (false, filename)
    3337    | Some filename' -> (true, filename') in
    3438  let save ?(suffix="") ast =
    35     Languages.save exact_output output_filename suffix ast
     39    Languages.save
     40      (Options.is_asm_pretty ()) exact_output output_filename suffix ast
    3641  in
    3742  let target_asts =
     
    4550  if Options.annotation_requested () then
    4651    begin
    47       let (annotated_input_ast, cost_id, cost_incr) =
     52      let (annotated_input_ast, cost_id, cost_incr, extern_cost_variables) =
    4853        Languages.annotate input_ast final_ast in (
    4954          save ~suffix:"-annotated" annotated_input_ast;
    50           Languages.save_cost output_filename cost_id cost_incr);
     55          Languages.save_cost exact_output output_filename cost_id cost_incr
     56            extern_cost_variables);
    5157    end;
    5258                                             
     
    5460    List.iter save intermediate_asts;
    5561
    56   if Options.interpretation_requested () || Options.is_debug_enabled () then
     62  if Options.interpretations_requested () then
    5763    begin
    5864      let asts = target_asts in
     
    6268      Checker.same_traces (List.combine asts label_traces);
    6369      Printf.eprintf "OK.\n%!";
    64     end
     70    end;
     71
     72  if Options.interpretation_requested () then
     73    ignore (Languages.interpret (Options.is_debug_enabled ()) final_ast)
     74
     75let lustre_test filename =
     76  let lustre_test       = match Options.get_lustre_test () with
     77    | None -> assert false (* do not use on this argument *)
     78    | Some lustre_test -> lustre_test in
     79  let lustre_test_cases = Options.get_lustre_test_cases () in
     80  let lustre_test_cycles = Options.get_lustre_test_cycles () in
     81  let lustre_test_min_int = Options.get_lustre_test_min_int () in
     82  let lustre_test_max_int = Options.get_lustre_test_max_int () in
     83  let src_language      = Languages.Clight in
     84  let tgt_language      = Languages.Clight in
     85  let input_ast         = Languages.parse src_language filename in
     86  let input_ast         =
     87    Languages.add_lustre_main lustre_test lustre_test_cases lustre_test_cycles
     88      lustre_test_min_int lustre_test_max_int input_ast in
     89  let (exact_output, output_filename) = match Options.get_output_files () with
     90    | None -> (false, filename)
     91    | Some filename' -> (true, filename') in
     92  let save ast =
     93    Languages.save
     94      (Options.is_asm_pretty ()) exact_output output_filename "" ast in
     95  let target_asts = Languages.compile false src_language tgt_language input_ast
     96  in
     97  let final_ast, _ = Misc.ListExt.cut_last target_asts in
     98  save input_ast ;
     99  save final_ast
    65100
    66101let _ =
    67102  if Options.is_dev_test_enabled () then Dev_test.do_dev_test input_files
    68   else List.iter process input_files
     103  else
     104    if Options.get_lustre_test () <> None then List.iter lustre_test input_files
     105    else List.iter process input_files
Note: See TracChangeset for help on using the changeset viewer.