Ignore:
Timestamp:
Oct 25, 2011, 4:11:11 PM (9 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/languages.ml

    r818 r1462  
    5151  | language -> [to_string language]
    5252
    53 let parse = function
     53let parse ?is_lustre_file ?remove_lustre_externals = function
    5454  | Clight ->
    55     fun filename -> AstClight (ClightParser.process filename)
     55    fun filename ->
     56      AstClight
     57        (ClightParser.process ?is_lustre_file ?remove_lustre_externals filename)
    5658
    5759(*
     
    111113
    112114let ltl_to_lin = function
    113   | AstLTL p -> 
     115  | AstLTL p ->
    114116    AstLIN (LTLToLIN.translate p)
    115117  | _ -> assert false
    116118
    117119let lin_to_asm = function
    118   | AstLIN p -> 
     120  | AstLIN p ->
    119121    AstASM (LINToASM.translate p)
    120122  | _ -> assert false
     
    210212let instrument costs_mapping = function
    211213  | AstClight p ->
    212     let (p', cost_id, cost_incr) = ClightAnnotator.instrument p costs_mapping in
    213     (AstClight p', cost_id, cost_incr)
     214    let (p', cost_id, cost_incr, extern_cost_variables) =
     215      ClightAnnotator.instrument p costs_mapping in
     216    (AstClight p', cost_id, cost_incr, extern_cost_variables)
    214217(*
    215218  | AstCminor p ->
     
    222225         "Instrumentation is not implemented for source language `%s'."
    223226         (to_string (language_of_ast p)));
    224     (p, "", "")
    225 
    226 let annotate input_ast final = 
     227    (p, "", "", StringTools.Map.empty)
     228
     229let annotate input_ast final =
    227230  let costs_mapping = compute_costs final in
    228231  instrument costs_mapping input_ast
    229232
    230 let string_output = function
     233let string_output asm_pretty = function
    231234  | AstClight p ->
    232235    [ClightPrinter.print_program p]
     
    244247    [LINPrinter.print_program p]
    245248  | AstASM p ->
    246     [Pretty.print_program p ; ASMPrinter.print_program p]
    247 
    248 let save exact_output filename suffix ast =
     249    (if asm_pretty then [Pretty.print_program p]
     250     else ["Pretty print not requested"]) @
     251    [ASMPrinter.print_program p]
     252
     253let save asm_pretty exact_output filename suffix ast =
    249254  let ext_chopped_filename =
    250255    if exact_output then filename
     
    259264    if exact_output then ext_filenames
    260265    else List.map Misc.SysExt.alternative ext_filenames in
    261   let output_strings = string_output ast in
     266  let output_strings = string_output asm_pretty ast in
    262267  let f filename s =
    263268    let cout = open_out filename in
     
    267272  List.iter2 f output_filenames output_strings
    268273
    269 let save_cost filename cost_id cost_incr =
     274let save_cost exact_name filename cost_id cost_incr extern_cost_variables =
     275  let filename =
     276    if exact_name then filename
     277    else
     278      try Filename.chop_extension filename
     279      with Invalid_argument ("Filename.chop_extension") -> filename in
    270280  let cout = open_out (filename ^ ".cerco") in
     281  let f fun_name cost_var =
     282    output_string cout (fun_name ^ " " ^ cost_var ^ "\n") in
    271283  output_string cout (cost_id ^ "\n");
    272284  output_string cout (cost_incr ^ "\n");
     285  StringTools.Map.iter f extern_cost_variables;
    273286  flush cout;
    274287  close_out cout
     
    291304  | AstASM p ->
    292305    ASMInterpret.interpret debug p
     306
     307let add_lustre_main
     308    lustre_test lustre_test_cases lustre_test_cycles
     309    lustre_test_min_int lustre_test_max_int = function
     310  | AstClight p ->
     311    AstClight
     312      (ClightLustreMain.add lustre_test lustre_test_cases lustre_test_cycles
     313         lustre_test_min_int lustre_test_max_int p)
     314  | _ ->
     315    Error.global_error "during main generation"
     316      "Lustre testing is only available with C programs."
Note: See TracChangeset for help on using the changeset viewer.