Changeset 3020


Ignore:
Timestamp:
Mar 28, 2013, 5:28:48 PM (4 years ago)
Author:
sacerdot
Message:
  • Options not used removed from the help/interface.
  • More compliance with the untrusted prototype.
Location:
driver
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • driver/acc.ml

    r3015 r3020  
    5656  match Extracted.Compiler.compile observe cl with
    5757  | OK o -> o
    58   | Error m -> failwith (Error.errormsg m)
    59 in
    60 let labelled = output.Extracted.Compiler.c_labelled_clight in
    61 let l_costmap = output.Extracted.Compiler.c_clight_cost_map in
    62 let s_costmap = output.Extracted.Compiler.c_stack_cost in
    63 let style = Cost_instrumented (l_costmap,s_costmap) in
    64 let instrumented = ClightPrinter.print_program style labelled in
    65 let filename = Filename.chop_extension filename ^ "-instrumented.c" in
    66 let och = open_out filename in
    67 output_string och instrumented;
    68 close_out och
     58  | Error m -> failwith (Error.errormsg m) in
     59if Options.annotation_requested () then
     60 begin
     61  let labelled = output.Extracted.Compiler.c_labelled_clight in
     62  let l_costmap = output.Extracted.Compiler.c_clight_cost_map in
     63  let s_costmap = output.Extracted.Compiler.c_stack_cost in
     64  let style = Cost_instrumented (l_costmap,s_costmap) in
     65  let instrumented = ClightPrinter.print_program style labelled in
     66  let filename = Filename.chop_extension filename ^ "-instrumented.c" in
     67  let och = open_out filename in
     68  output_string och instrumented;
     69  close_out och
     70 end
    6971) (OptionsParsing.results ())
  • driver/options.ml

    r3005 r3020  
    22let extra_doc s = "", Arg.Unit ignore, s
    33
     4(*
    45let web_mode             = ref false
    56let is_web_mode ()       = !web_mode
    67let set_web_mode ()      = web_mode := true
     8*)
    79
     10(*
    811let default_choice       = "default"
    912let option_settings_step = "during option settings"
    1013
    11 (*
    1214let language_from_string kind default s =
    1315  try
     
    3133*)
    3234
     35(*
    3336let input_files                 = ref []
    3437let add_input_file f            = input_files := f :: !input_files
    3538let input_files ()              = !input_files
     39*)
    3640
    3741let output_files                = ref None
     
    4347let annotation_requested ()     = !annotation_flag
    4448
     49(*
    4550let interpretation_flag         = ref false
    4651let request_interpretation      = (:=) interpretation_flag
    4752let interpretation_requested () = !interpretation_flag
     53*)
    4854
    4955let interpretations_flag         = ref false
     
    5157let interpretations_requested () = !interpretations_flag
    5258
     59(*
    5360let debug_flag                  = ref false
    5461let set_debug                   = (:=) debug_flag
    5562let is_debug_enabled ()         = !debug_flag
     63*)
    5664
     65(*
    5766let asm_pretty_flag             = ref false
    5867let set_asm_pretty              = (:=) asm_pretty_flag
    5968let is_asm_pretty ()            = !asm_pretty_flag
     69*)
    6070
    6171let lustre_flag                 = ref false
     
    93103*)
    94104
     105(*
    95106let dev_test                    = ref false
    96107let set_dev_test                = (:=) dev_test
    97108let is_dev_test_enabled ()      = !dev_test
     109*)
    98110
    99111let options = OptionsParsing.register [
     
    113125  " Add cost annotations on the source code.";
    114126
     127(*
    115128  "-i", Arg.Set interpretation_flag,
    116129  " Interpret the compiled code.";
     130*)
    117131
    118132  "-is", Arg.Set interpretations_flag,
    119   " Interpret all the compilation passes.";
     133  " Outputs and interprets all the compilation passes,";
     134  extra_doc " showing the execution traces";
    120135
     136(*
    121137  "-d", Arg.Set debug_flag,
    122138  " Debug mode.";
     
    124140  extra_doc " Combined with an interpret option, shows the trace";
    125141  extra_doc " of execution states.";
     142*)
    126143
    127144  "-o", Arg.String set_output_files,
    128145  " Prefix of the output files.";
    129146
     147(*
    130148  "-asm-pretty", Arg.Set asm_pretty_flag,
    131149  " Output a pretty-printed assembly file.";
     150*)
    132151
    133152  "-lustre", Arg.Set lustre_flag,
     
    163182*)
    164183
     184(*
    165185  "-dev", Arg.Set dev_test,
    166186  " Playground for developers.";
     187*)
    167188]
  • driver/options.mli

    r3005 r3020  
    1111*)
    1212
     13(*
    1314(** {2 Interpretation request} *)
    1415val request_interpretation   : bool -> unit
    1516val interpretation_requested : unit -> bool
     17*)
    1618
    1719(** {2 Interpretation requests} *)
     
    2325val annotation_requested : unit -> bool
    2426
     27(*
    2528(** {2 Input files} *)
    2629val add_input_file : string -> unit
    2730val input_files    : unit -> string list
     31*)
    2832
    2933(** {2 Output files} *)
     
    3135val get_output_files : unit -> string option
    3236
     37(*
    3338(** {2 Verbose mode} *)
    3439val is_debug_enabled : unit -> bool
     40*)
    3541
     42(*
    3643(** {2 Assembly pretty print} *)
    3744val set_asm_pretty : bool -> unit
    3845val is_asm_pretty  : unit -> bool
     46*)
    3947
    4048(** {2 Lustre file} *)
     
    7179*)
    7280
     81(*
    7382(** {2 Developers' playground} *)
    7483val is_dev_test_enabled : unit -> bool
     84*)
    7585
     86(*
    7687(** {2 Web application} *)
    7788val set_web_mode : unit -> unit
    7889val is_web_mode  : unit -> bool
     90*)
Note: See TracChangeset for help on using the changeset viewer.